let L be complete Lattice; :: thesis: for f being monotone UnOp of L holds FixPoints f is complete
let f be monotone UnOp of L; :: thesis: FixPoints f is complete
set F = FixPoints f;
set cF = the carrier of (FixPoints f);
set cL = the carrier of L;
A1: the carrier of (FixPoints f) = { x where x is Element of L : x is_a_fixpoint_of f } by Th39;
let X be set ; :: according to LATTICE3:def 18 :: thesis: ex b₁ being Element of the carrier of (FixPoints f) st
( X is_less_than b₁ & ( for b₂ being Element of the carrier of (FixPoints f) holds
( not X is_less_than b₂ or b₁ [= b₂ ) ) )
set Y = X /\ the carrier of (FixPoints f);
A2: ( X /\ the carrier of (FixPoints f) c= X & X /\ the carrier of (FixPoints f) c= the carrier of (FixPoints f) ) by XBOOLE_1:17;
set s = "\/" (X /\ the carrier of (FixPoints f)),L;
X /\ the carrier of (FixPoints f) is_less_than f . ("\/" (X /\ the carrier of (FixPoints f)),L)

proof

let q be Element of the carrier of L; :: according to LATTICE3:def 17 :: thesis: ( not q in X /\ the carrier of (FixPoints f) or q [= f . ("\/" (X /\ the carrier of (FixPoints f)),L) )
assume A3: q in X /\ the carrier of (FixPoints f) ; :: thesis: q [= f . ("\/" (X /\ the carrier of (FixPoints f)),L)
then q [= "\/" (X /\ the carrier of (FixPoints f)),L by LATTICE3:38;
then A4: f . q [= f . ("\/" (X /\ the carrier of (FixPoints f)),L) by QUANTAL1:def 12;
reconsider q' = q as Element of L ;
q' is_a_fixpoint_of f by A2, A3, Th41;
hence q [= f . ("\/" (X /\ the carrier of (FixPoints f)),L) by A4, ABIAN:def 3; :: thesis: verum

end;

then A5: "\/" (X /\ the carrier of (FixPoints f)),L [= f . ("\/" (X /\ the carrier of (FixPoints f)),L) by LATTICE3:def 21;
then consider O being Ordinal such that
A6: ( card O c= card the carrier of L & f,O +. ("\/" (X /\ the carrier of (FixPoints f)),L) is_a_fixpoint_of f ) by Th33;
reconsider p' = f,O +. ("\/" (X /\ the carrier of (FixPoints f)),L) as Element of L ;
reconsider p = p' as Element of the carrier of (FixPoints f) by A6, Th41;
take p ; :: thesis: ( X is_less_than p & ( for b₁ being Element of the carrier of (FixPoints f) holds
( not X is_less_than b₁ or p [= b₁ ) ) )
thus X is_less_than p :: thesis: for b₁ being Element of the carrier of (FixPoints f) holds
( not X is_less_than b₁ or p [= b₁ )

proof

let q be Element of the carrier of (FixPoints f); :: according to LATTICE3:def 17 :: thesis: ( not q in X or q [= p )
assume A7: q in X ; :: thesis: q [= p
( q in the carrier of (FixPoints f) & the carrier of (FixPoints f) c= the carrier of L ) by Th40;
then reconsider qL' = q as Element of L ;
q in X /\ the carrier of (FixPoints f) by A7, XBOOLE_0:def 4;
then A8: qL' [= "\/" (X /\ the carrier of (FixPoints f)),L by LATTICE3:38;
"\/" (X /\ the carrier of (FixPoints f)),L [= p' by A5, Th25;
then qL' [= p' by A8, LATTICES:25;
hence q [= p by Th42; :: thesis: verum

end;

let r be Element of the carrier of (FixPoints f); :: thesis: ( not X is_less_than r or p [= r )
assume A9: X is_less_than r ; :: thesis: p [= r
r in the carrier of (FixPoints f) ;
then consider r' being Element of L such that
A10: ( r' = r & r' is_a_fixpoint_of f ) by A1;
reconsider r'' = r as Element of (FixPoints f) ;
X /\ the carrier of (FixPoints f) is_less_than r'

proof

let q be Element of the carrier of L; :: according to LATTICE3:def 17 :: thesis: ( not q in X /\ the carrier of (FixPoints f) or q [= r' )
assume A11: q in X /\ the carrier of (FixPoints f) ; :: thesis: q [= r'
then reconsider q'' = q as Element of (FixPoints f) by A2;
q'' [= r'' by A2, A9, A11, LATTICE3:def 17;
hence q [= r' by A10, Th42; :: thesis: verum

end;

then "\/" (X /\ the carrier of (FixPoints f)),L [= r' by LATTICE3:def 21;
then p' [= r' by A5, A10, Th37;
hence p [= r by A10, Th42; :: thesis: verum