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 & dom (id S) = S & rng (id S) = S ) by RELAT_1:71, YELLOW_0:def 15;
hence id S is Function of (subrelstr S),L by FUNCT_2:4; :: 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 A2: 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 A3: [x,y] in the InternalRel of (subrelstr S) ; :: according to ORDERS_2:def 9 :: thesis: for b₁, b₂ being Element of the carrier of L holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ )
then A4: ( x in S & y in S ) by A1, ZFMISC_1:106;
let a, b be Element of L; :: thesis: ( not a = f . x or not b = f . y or a <= b )
assume ( a = f . x & b = f . y ) ; :: thesis: a <= b
then ( a = x & b = y & the InternalRel of (subrelstr S) c= the InternalRel of L ) by A2, A4, FUNCT_1:34, YELLOW_0:def 13;
hence [a,b] in the InternalRel of L by A3; :: according to ORDERS_2:def 9 :: thesis: verum