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 b_{1} being Element of the carrier of (FixPoints f) st

( X is_less_than b_{1} & ( for b_{2} being Element of the carrier of (FixPoints f) holds

( not X is_less_than b_{2} or b_{1} [= b_{2} ) ) )

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))

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 b_{1} being Element of the carrier of (FixPoints f) holds

( not X is_less_than b_{1} or p [= b_{1} ) ) )

thus X is_less_than p :: thesis: for b_{1} being Element of the carrier of (FixPoints f) holds

( not X is_less_than b_{1} or p [= b_{1} )

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

then p9 [= r9 by A9, Th34;

hence p [= r by A8, Th39; :: thesis: verum

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 b

( X is_less_than b

( not X is_less_than b

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

then A4:
"\/" ((X /\ the carrier of (FixPoints f)),L) [= f . ("\/" ((X /\ the carrier of (FixPoints f)),L))
by LATTICE3:def 21;
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;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

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 b

( not X is_less_than b

thus X is_less_than p :: thesis: for b

( not X is_less_than b

proof

let r be Element of the carrier of (FixPoints f); :: thesis: ( not X is_less_than r or p [= r )
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;( 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

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

then
"\/" ((X /\ the carrier of (FixPoints f)),L) [= r9
by LATTICE3:def 21;
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;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

then p9 [= r9 by A9, Th34;

hence p [= r by A8, Th39; :: thesis: verum