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 & a [= (f,O) +. (a "\/" b) & b [= (f,O) +. (a "\/" 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 & a [= (f,O) +. (a "\/" b) & b [= (f,O) +. (a "\/" 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 & a [= (f,O) +. (a "\/" b) & b [= (f,O) +. (a "\/" b) ) )

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

A1: a [= ab by LATTICES:5;

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

A3: b [= ab by LATTICES:5;

then A4: f . b [= f . ab 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 & a [= (f,O) +. (a "\/" b) & b [= (f,O) +. (a "\/" 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, Th30, FILTER_0:6;

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

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

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

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

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

thus b [= (f,O) +. (a "\/" 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 & a [= (f,O) +. (a "\/" b) & b [= (f,O) +. (a "\/" 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 & a [= (f,O) +. (a "\/" b) & b [= (f,O) +. (a "\/" 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 & a [= (f,O) +. (a "\/" b) & b [= (f,O) +. (a "\/" b) ) )

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

A1: a [= ab by LATTICES:5;

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

A3: b [= ab by LATTICES:5;

then A4: f . b [= f . ab 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 & a [= (f,O) +. (a "\/" b) & b [= (f,O) +. (a "\/" 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, Th30, FILTER_0:6;

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

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

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

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

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

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