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;
let X be set ; :: according to LATTICE3:def 18 :: thesis: ex b1 being Element of the carrier of (FixPoints f) st
( X is_less_than b1 & ( for b2 being Element of the carrier of (FixPoints f) holds
( not X is_less_than b2 or b1 [= b2 ) ) )
set Y = X /\ the carrier of (FixPoints f);
set s = "\/" ((X /\ the carrier of (FixPoints f)),L);
A1: X /\ the carrier of (FixPoints f) c= the carrier of (FixPoints f) by XBOOLE_1:17;
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)) )
reconsider q9 = q as Element of L ;
assume A2: 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 A3: f . q [= f . ("\/" ((X /\ the carrier of (FixPoints f)),L)) by QUANTAL1:def 12;
q9 is_a_fixpoint_of f by A1, A2, Th38;
hence q [= f . ("\/" ((X /\ the carrier of (FixPoints f)),L)) by A3; :: thesis: verum
end;
then A4: "\/" ((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
card O c= card the carrier of L and
A5: (f,O) +. ("\/" ((X /\ the carrier of (FixPoints f)),L)) is_a_fixpoint_of f by Th30;
reconsider p9 = (f,O) +. ("\/" ((X /\ the carrier of (FixPoints f)),L)) as Element of L ;
reconsider p = p9 as Element of the carrier of (FixPoints f) by A5, Th38;
take p ; :: thesis: ( X is_less_than p & ( for b1 being Element of the carrier of (FixPoints f) holds
( not X is_less_than b1 or p [= b1 ) ) )
thus X is_less_than p :: thesis: for b1 being Element of the carrier of (FixPoints f) holds
( not X is_less_than b1 or p [= b1 )
proof
let q be Element of the carrier of (FixPoints f); :: according to LATTICE3:def 17 :: thesis: ( not q in X or q [= p )
( q in the carrier of (FixPoints f) & the carrier of (FixPoints f) c= the carrier of L ) by Th37;
then reconsider qL9 = q as Element of L ;
assume q in X ; :: thesis: q [= p
then q in X /\ the carrier of (FixPoints f) by XBOOLE_0:def 4;
then A6: qL9 [= "\/" ((X /\ the carrier of (FixPoints f)),L) by LATTICE3:38;
"\/" ((X /\ the carrier of (FixPoints f)),L) [= p9 by A4, Th22;
then qL9 [= p9 by A6, LATTICES:7;
hence q [= p by Th39; :: thesis: verum
end;
let r be Element of the carrier of (FixPoints f); :: thesis: ( not X is_less_than r or p [= r )
assume A7: X is_less_than r ; :: thesis: p [= r
reconsider r99 = r as Element of (FixPoints f) ;
( the carrier of (FixPoints f) = { x where x is Element of L : x is_a_fixpoint_of f } & r in the carrier of (FixPoints f) ) by Th36;
then consider r9 being Element of L such that
A8: r9 = r and
A9: r9 is_a_fixpoint_of f ;
A10: X /\ the carrier of (FixPoints f) c= X by XBOOLE_1:17;
X /\ the carrier of (FixPoints f) is_less_than r9
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 [= r9 )
assume A11: q in X /\ the carrier of (FixPoints f) ; :: thesis: q [= r9
then reconsider q99 = q as Element of (FixPoints f) by A1;
q99 [= r99 by A10, A7, A11;
hence q [= r9 by A8, Th39; :: thesis: verum
end;
then "\/" ((X /\ the carrier of (FixPoints f)),L) [= r9 by LATTICE3:def 21;
then p9 [= r9 by A9, Th34;
hence p [= r by A8, Th39; :: thesis: verum