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