let L be RelStr ; :: thesis: for S being Subset of L holds
( id S is Function of (),L & ( for f being Function of (),L st f = id S holds
f is monotone ) )

let S be Subset of L; :: thesis: ( id S is Function of (),L & ( for f being Function of (),L st f = id S holds
f is monotone ) )

A1: the carrier of () = S by YELLOW_0:def 15;
A2: rng (id S) = S by RELAT_1:45;
dom (id S) = S by RELAT_1:45;
hence id S is Function of (),L by ; :: thesis: for f being Function of (),L st f = id S holds
f is monotone

let f be Function of (),L; :: thesis: ( f = id S implies f is monotone )
assume A3: f = id S ; :: thesis: f is monotone
let x, y be Element of (); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) )

assume A4: [x,y] in the InternalRel of () ; :: according to ORDERS_2:def 5 :: thesis: for b1, b2 being Element of the carrier of L holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 )

let a, b be Element of L; :: thesis: ( not a = f . x or not b = f . y or a <= b )
assume that
A5: a = f . x and
A6: b = f . y ; :: thesis: a <= b
x in S by ;
then A7: a = x by ;
y in S by ;
then A8: b = y by ;
the InternalRel of () c= the InternalRel of L by YELLOW_0:def 13;
hence [a,b] in the InternalRel of L by A4, A7, A8; :: according to ORDERS_2:def 5 :: thesis: verum