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₁, b₂ being Element of the carrier of L holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ ) )
assume A4: [x,y] in the InternalRel of (subrelstr S) ; :: according to ORDERS_2:def 5 :: thesis: for b₁, b₂ being Element of the carrier of L holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= 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