let L be RelStr ; :: thesis: for S being Subset of L holds

( id S is Function of (subrelstr S),L & ( for f being Function of (subrelstr S),L st f = id S holds

f is monotone ) )

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

f is monotone ) )

A1: the carrier of (subrelstr S) = 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 (subrelstr S),L by A1, A2, FUNCT_2:2; :: thesis: for f being Function of (subrelstr S),L st f = id S holds

f is monotone

let f be Function of (subrelstr S),L; :: thesis: ( f = id S implies f is monotone )

assume A3: f = id S ; :: thesis: f is monotone

let x, y be Element of (subrelstr S); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b_{1}, b_{2} being Element of the carrier of L holds

( not b_{1} = f . x or not b_{2} = f . y or b_{1} <= b_{2} ) )

assume A4: [x,y] in the InternalRel of (subrelstr S) ; :: according to ORDERS_2:def 5 :: thesis: for b_{1}, b_{2} being Element of the carrier of L holds

( not b_{1} = f . x or not b_{2} = f . y or b_{1} <= b_{2} )

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 A1, A4, ZFMISC_1:87;

then A7: a = x by A3, A5, FUNCT_1:17;

y in S by A1, A4, ZFMISC_1:87;

then A8: b = y by A3, A6, FUNCT_1:17;

the InternalRel of (subrelstr S) 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

( id S is Function of (subrelstr S),L & ( for f being Function of (subrelstr S),L st f = id S holds

f is monotone ) )

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

f is monotone ) )

A1: the carrier of (subrelstr S) = 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 (subrelstr S),L by A1, A2, FUNCT_2:2; :: thesis: for f being Function of (subrelstr S),L st f = id S holds

f is monotone

let f be Function of (subrelstr S),L; :: thesis: ( f = id S implies f is monotone )

assume A3: f = id S ; :: thesis: f is monotone

let x, y be Element of (subrelstr S); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b

( not b

assume A4: [x,y] in the InternalRel of (subrelstr S) ; :: according to ORDERS_2:def 5 :: thesis: for b

( not b

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 A1, A4, ZFMISC_1:87;

then A7: a = x by A3, A5, FUNCT_1:17;

y in S by A1, A4, ZFMISC_1:87;

then A8: b = y by A3, A6, FUNCT_1:17;

the InternalRel of (subrelstr S) 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