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) ) )
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 A1: ( a = f . a & b = f . b ) by ABIAN:def 3;
reconsider ab = a "\/" b as Element of L ;
A2: ( a [= ab & b [= ab ) by LATTICES:22;
then ( f . a [= f . ab & f . b [= f . ab ) by QUANTAL1:def 12;
then A3: ab [= f . ab by A1, FILTER_0:6;
then consider O being Ordinal such that
A4: ( card O c= card the carrier of L & f,O +. ab is_a_fixpoint_of f ) by Th33;
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 A4; :: thesis: ( a [= f,O +. (a "\/" b) & b [= f,O +. (a "\/" b) )
A5: ab [= f,O +. (a "\/" b) by A3, Th25;
hence a [= f,O +. (a "\/" b) by A2, LATTICES:25; :: thesis: b [= f,O +. (a "\/" b)
thus b [= f,O +. (a "\/" b) by A2, A5, LATTICES:25; :: thesis: verum