let L be complete Lattice; :: thesis: for f being monotone UnOp of L ex a being Element of L st a is_a_fixpoint_of f
let f be monotone UnOp of L; :: thesis: ex a being Element of L st a is_a_fixpoint_of f
set H = { h where h is Element of L : h [= f . h } ;
set fH = { (f . h) where h is Element of L : h [= f . h } ;
set uH = "\/" { h where h is Element of L : h [= f . h } ,L;
set fuH = "\/" { (f . h) where h is Element of L : h [= f . h } ,L;
take "\/" { h where h is Element of L : h [= f . h } ,L ; :: thesis: "\/" { h where h is Element of L : h [= f . h } ,L is_a_fixpoint_of f

now

let a be Element of L; :: thesis: ( a in { h where h is Element of L : h [= f . h } implies ex fh being Element of L st
( a [= fh & fh in { (f . h) where h is Element of L : h [= f . h } ) )
assume a in { h where h is Element of L : h [= f . h } ; :: thesis: ex fh being Element of L st
( a [= fh & fh in { (f . h) where h is Element of L : h [= f . h } )
then consider h being Element of L such that
A1: ( a = h & h [= f . h ) ;
reconsider fh = f . h as Element of L ;
take fh = fh; :: thesis: ( a [= fh & fh in { (f . h) where h is Element of L : h [= f . h } )
thus ( a [= fh & fh in { (f . h) where h is Element of L : h [= f . h } ) by A1; :: thesis: verum

end;

then A2: "\/" { h where h is Element of L : h [= f . h } ,L [= "\/" { (f . h) where h is Element of L : h [= f . h } ,L by LATTICE3:48;

now

let fh be Element of L; :: thesis: ( fh in { (f . h) where h is Element of L : h [= f . h } implies fh [= f . ("\/" { h where h is Element of L : h [= f . h } ,L) )
assume fh in { (f . h) where h is Element of L : h [= f . h } ; :: thesis: fh [= f . ("\/" { h where h is Element of L : h [= f . h } ,L)
then consider h being Element of L such that
A3: ( fh = f . h & h [= f . h ) ;
h in { h where h is Element of L : h [= f . h } by A3;
then h [= "\/" { h where h is Element of L : h [= f . h } ,L by LATTICE3:38;
hence fh [= f . ("\/" { h where h is Element of L : h [= f . h } ,L) by A3, QUANTAL1:def 12; :: thesis: verum

end;

then { (f . h) where h is Element of L : h [= f . h } is_less_than f . ("\/" { h where h is Element of L : h [= f . h } ,L) by LATTICE3:def 17;
then "\/" { (f . h) where h is Element of L : h [= f . h } ,L [= f . ("\/" { h where h is Element of L : h [= f . h } ,L) by LATTICE3:def 21;
then A4: "\/" { h where h is Element of L : h [= f . h } ,L [= f . ("\/" { h where h is Element of L : h [= f . h } ,L) by A2, LATTICES:25;
then f . ("\/" { h where h is Element of L : h [= f . h } ,L) [= f . (f . ("\/" { h where h is Element of L : h [= f . h } ,L)) by QUANTAL1:def 12;
then f . ("\/" { h where h is Element of L : h [= f . h } ,L) in { h where h is Element of L : h [= f . h } ;
then f . ("\/" { h where h is Element of L : h [= f . h } ,L) [= "\/" { h where h is Element of L : h [= f . h } ,L by LATTICE3:38;
hence "\/" { h where h is Element of L : h [= f . h } ,L = f . ("\/" { h where h is Element of L : h [= f . h } ,L) by A4, LATTICES:26; :: according to ABIAN:def 4 :: thesis: verum