let L be complete Lattice; :: thesis: for f being monotone UnOp of L

for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds

ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f & (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b )

let f be monotone UnOp of L; :: thesis: for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds

ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f & (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b )

let a, b be Element of L; :: thesis: ( a is_a_fixpoint_of f & b is_a_fixpoint_of f implies ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f & (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b ) )

reconsider ab = a "/\" b as Element of L ;

A1: ab [= a by LATTICES:6;

then A2: f . ab [= f . a by QUANTAL1:def 12;

A3: ab [= b by LATTICES:6;

then A4: f . ab [= f . b by QUANTAL1:def 12;

assume ( a is_a_fixpoint_of f & b is_a_fixpoint_of f ) ; :: thesis: ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f & (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b )

then A5: ( a = f . a & b = f . b ) ;

then consider O being Ordinal such that

A6: ( card O c= card the carrier of L & (f,O) -. ab is_a_fixpoint_of f ) by A2, A4, Th31, FILTER_0:7;

take O ; :: thesis: ( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f & (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b )

thus ( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f ) by A6; :: thesis: ( (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b )

f . ab [= ab by A5, A2, A4, FILTER_0:7;

then A7: (f,O) -. (a "/\" b) [= ab by Th23;

hence (f,O) -. (a "/\" b) [= a by A1, LATTICES:7; :: thesis: (f,O) -. (a "/\" b) [= b

thus (f,O) -. (a "/\" b) [= b by A3, A7, LATTICES:7; :: thesis: verum

for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds

ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f & (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b )

let f be monotone UnOp of L; :: thesis: for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds

ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f & (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b )

let a, b be Element of L; :: thesis: ( a is_a_fixpoint_of f & b is_a_fixpoint_of f implies ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f & (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b ) )

reconsider ab = a "/\" b as Element of L ;

A1: ab [= a by LATTICES:6;

then A2: f . ab [= f . a by QUANTAL1:def 12;

A3: ab [= b by LATTICES:6;

then A4: f . ab [= f . b by QUANTAL1:def 12;

assume ( a is_a_fixpoint_of f & b is_a_fixpoint_of f ) ; :: thesis: ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f & (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b )

then A5: ( a = f . a & b = f . b ) ;

then consider O being Ordinal such that

A6: ( card O c= card the carrier of L & (f,O) -. ab is_a_fixpoint_of f ) by A2, A4, Th31, FILTER_0:7;

take O ; :: thesis: ( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f & (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b )

thus ( card O c= card the carrier of L & (f,O) -. (a "/\" b) is_a_fixpoint_of f ) by A6; :: thesis: ( (f,O) -. (a "/\" b) [= a & (f,O) -. (a "/\" b) [= b )

f . ab [= ab by A5, A2, A4, FILTER_0:7;

then A7: (f,O) -. (a "/\" b) [= ab by Th23;

hence (f,O) -. (a "/\" b) [= a by A1, LATTICES:7; :: thesis: (f,O) -. (a "/\" b) [= b

thus (f,O) -. (a "/\" b) [= b by A3, A7, LATTICES:7; :: thesis: verum