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 ) )
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 A1: ( a = f . a & b = f . b ) by ABIAN:def 3;
reconsider ab = a "/\" b as Element of L ;
A2: ( ab [= a & ab [= b ) by LATTICES:23;
then ( f . ab [= f . a & f . ab [= f . b ) by QUANTAL1:def 12;
then A3: f . ab [= ab by A1, FILTER_0:7;
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 Th34;
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 A4; :: thesis: ( f,O -. (a "/\" b) [= a & f,O -. (a "/\" b) [= b )
A5: f,O -. (a "/\" b) [= ab by A3, Th26;
hence f,O -. (a "/\" b) [= a by A2, LATTICES:25; :: thesis: f,O -. (a "/\" b) [= b
thus f,O -. (a "/\" b) [= b by A2, A5, LATTICES:25; :: thesis: verum