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