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: 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, Th22;
then f . (inf Y) <= f . y by A1, A7;
hence f . (inf Y) <= u by A7, A8, ORDERS_2:3; :: thesis: verum

end;

A9: 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 A10: m in X ; :: thesis: m <= f . (f . (inf Y))
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
A11: y = u and
A12: X is_<=_than f . y and
A13: f . y <= y by A4;
m <= f . y by A10, A12;
hence m <= u by A11, A13, ORDERS_2:3; :: thesis: verum

end;

then m <= inf Y by YELLOW_0:33;
then A14: f . m <= f . (inf Y) by A1;
X c= the carrier of (subrelstr M) ;
then X c= M by YELLOW_0:def 15;
then m in M by A10;
then ex x being Element of L st
( x = m & x = f . x ) by A2;
hence m <= f . (f . (inf Y)) by A1, A14; :: thesis: verum

end;

ex_inf_of Y,L by YELLOW_0:17;
then A15: f . (inf Y) <= inf Y by A5, YELLOW_0:31;
then f . (f . (inf Y)) <= f . (inf Y) by A1;
then f . (inf Y) in Y by A4, A9;
then inf Y <= f . (inf Y) by Th22;
then inf Y = f . (inf Y) by A15, ORDERS_2:2;
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 by A3;
then reconsider z = inf Y as Element of S ;
A16: X is_<=_than z

proof

let x be Element of S; :: according to LATTICE3:def 9 :: thesis: ( not x in X or 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
A17: x = m and
m = f . m by A2;
assume A18: x in X ; :: thesis: x <= z
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
A19: y = u and
A20: X is_<=_than f . y and
A21: f . y <= y ;
m <= f . y by A18, A17, A20;
hence m <= u by A19, A21, ORDERS_2:3; :: thesis: verum

end;

then m <= inf Y by YELLOW_0:33;
hence x <= z by A17, YELLOW_0:60; :: 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
A22: x = b and
A23: x = f . x by A2;
assume X is_<=_than b ; :: thesis: z <= b
then X is_<=_than f . x by A22, A23, YELLOW_0:62;
then x in Y by A23;
hence z <= b by A22, Th22, YELLOW_0:60; :: thesis: verum

end;

hence ex_sup_of X,S by A16, 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