let L be complete LATTICE; :: thesis: for f being Function of L,L st f is monotone holds
for M being Subset of L st M = { x where x is Element of L : x = f . x } holds
subrelstr M is complete LATTICE
let f be Function of L,L; :: thesis: ( f is monotone implies for M being Subset of L st M = { x where x is Element of L : x = f . x } holds
subrelstr M is complete LATTICE )
assume A1: f is monotone ; :: thesis: for M being Subset of L st M = { x where x is Element of L : x = f . x } holds
subrelstr M is complete LATTICE
let M be Subset of L; :: thesis: ( M = { x where x is Element of L : x = f . x } implies subrelstr M is complete LATTICE )
assume A2: M = { x where x is Element of L : x = f . x } ; :: thesis: subrelstr M is complete LATTICE
set S = subrelstr M;
A3: for X being Subset of (subrelstr M)
for Y being Subset of L st Y = { y where y is Element of L : ( X is_<=_than f . y & f . y <= y ) } holds
inf Y in M

proof

let X be Subset of (subrelstr M); :: thesis: for Y being Subset of L st Y = { y where y is Element of L : ( X is_<=_than f . y & f . y <= y ) } holds
inf Y in M
let Y be Subset of L; :: thesis: ( Y = { y where y is Element of L : ( X is_<=_than f . y & f . y <= y ) } implies inf Y in M )
assume A4: Y = { y where y is Element of L : ( X is_<=_than f . y & f . y <= y ) } ; :: thesis: inf Y in M
set z = inf Y;
A5: ex_inf_of Y,L by YELLOW_0:17;
f . (inf Y) is_<=_than Y

proof

let u be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not u in Y or f . (inf Y) <= u )
assume A6: u in Y ; :: thesis: f . (inf Y) <= u
then consider y being Element of L such that
A7: y = u and
X is_<=_than f . y and
A8: f . y <= y by A4;
inf Y <= u by A6, Th24;
then f . (inf Y) <= f . y by A1, A7, ORDERS_3:def 5;
hence f . (inf Y) <= u by A7, A8, ORDERS_2:26; :: thesis: verum

end;

then A9: f . (inf Y) <= inf Y by A5, YELLOW_0:31;
then A10: f . (f . (inf Y)) <= f . (inf Y) by A1, ORDERS_3:def 5;
X is_<=_than f . (f . (inf Y))

proof

let m be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not m in X or m <= f . (f . (inf Y)) )
assume A11: m in X ; :: thesis: m <= f . (f . (inf Y))
X c= the carrier of (subrelstr M) ;
then X c= M by YELLOW_0:def 15;
then m in M by A11;
then consider x being Element of L such that
A12: x = m and
A13: x = f . x by A2;
m is_<=_than Y

proof

let u be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not u in Y or m <= u )
assume u in Y ; :: thesis: m <= u
then consider y being Element of L such that
A14: y = u and
A15: X is_<=_than f . y and
A16: f . y <= y by A4;
m <= f . y by A11, A15, LATTICE3:def 9;
hence m <= u by A14, A16, ORDERS_2:26; :: thesis: verum

end;

then m <= inf Y by YELLOW_0:33;
then f . m <= f . (inf Y) by A1, ORDERS_3:def 5;
hence m <= f . (f . (inf Y)) by A1, A12, A13, ORDERS_3:def 5; :: thesis: verum

end;

then f . (inf Y) in Y by A4, A10;
then inf Y <= f . (inf Y) by Th24;
then inf Y = f . (inf Y) by A9, ORDERS_2:25;
hence inf Y in M by A2; :: thesis: verum

end;

M c= the carrier of (subrelstr M) by YELLOW_0:def 15;
then reconsider M = M as Subset of (subrelstr M) ;
defpred S₁[ Element of L] means ( M is_<=_than f . $1 & f . $1 <= $1 );
reconsider Y = { y where y is Element of L : S₁[y] } as Subset of L from DOMAIN_1:sch 7();
inf Y in M by A3;
then reconsider S = subrelstr M as non empty Poset ;
for X being Subset of S holds ex_sup_of X,S

proof

let X be Subset of S; :: thesis: ex_sup_of X,S
defpred S₂[ Element of L] means ( X is_<=_than f . $1 & f . $1 <= $1 );
reconsider Y = { y where y is Element of L : S₂[y] } as Subset of L from DOMAIN_1:sch 7();
set z = inf Y;
( inf Y in M & M = the carrier of S ) by A3, YELLOW_0:def 15;
then reconsider z = inf Y as Element of S ;
A17: X is_<=_than z

proof

let x be Element of S; :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= z )
assume A18: x in X ; :: thesis: x <= z
x in the carrier of S ;
then x in M by YELLOW_0:def 15;
then consider m being Element of L such that
A19: x = m and
m = f . m by A2;
m is_<=_than Y

proof

let u be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not u in Y or m <= u )
assume u in Y ; :: thesis: m <= u
then consider y being Element of L such that
A20: y = u and
A21: X is_<=_than f . y and
A22: f . y <= y ;
m <= f . y by A18, A19, A21, LATTICE3:def 9;
hence m <= u by A20, A22, ORDERS_2:26; :: thesis: verum

end;

then ( m <= inf Y & x in the carrier of S & z in the carrier of S ) by YELLOW_0:33;
hence x <= z by A19, YELLOW_0:61; :: thesis: verum

end;

for b being Element of S st X is_<=_than b holds
z <= b

proof

let b be Element of S; :: thesis: ( X is_<=_than b implies z <= b )
b in the carrier of S ;
then b in M by YELLOW_0:def 15;
then consider x being Element of L such that
A23: x = b and
A24: x = f . x by A2;
assume X is_<=_than b ; :: thesis: z <= b
then ( X is_<=_than f . x & f . x <= x ) by A23, A24, YELLOW_0:63;
then x in Y ;
then ( inf Y <= x & z in the carrier of S & b in the carrier of S ) by Th24;
hence z <= b by A23, YELLOW_0:61; :: thesis: verum

end;

hence ex_sup_of X,S by A17, YELLOW_0:30; :: thesis: verum

end;

then reconsider S = S as non empty complete Poset by YELLOW_0:53;
S is complete LATTICE ;
hence subrelstr M is complete LATTICE ; :: thesis: verum