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

then A3: "\/" ( { (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 A5: "\/" ( { h where h is Element of L : h [= f . h } ,L) [= f . ("\/" ( { h where h is Element of L : h [= f . h } ,L)) by A3, LATTICES:7;

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 A5, LATTICES:8; :: according to ABIAN:def 4 :: thesis: verum

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 :: thesis: for fh being Element of L st fh in { (f . h) where h is Element of L : h [= f . h } holds

fh [= f . ("\/" ( { h where h is Element of L : h [= f . h } ,L))

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))
;fh [= f . ("\/" ( { h where h is Element of L : h [= f . h } ,L))

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

A1: fh = f . h and

A2: h [= f . h ;

h in { h where h is Element of L : h [= f . h } by A2;

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 A1, QUANTAL1:def 12; :: thesis: verum

end;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

A1: fh = f . h and

A2: h [= f . h ;

h in { h where h is Element of L : h [= f . h } by A2;

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 A1, QUANTAL1:def 12; :: thesis: verum

then A3: "\/" ( { (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;

now :: thesis: for a being Element of L st a in { h where h is Element of L : h [= f . h } holds

ex fh being Element of L st

( a [= fh & fh in { (f . h) where h is Element of L : h [= f . h } )

then
"\/" ( { 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:47;ex fh being Element of L st

( a [= fh & fh in { (f . h) where h is Element of L : h [= f . h } )

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

A4: ( 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 A4; :: thesis: verum

end;( 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

A4: ( 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 A4; :: thesis: verum

then A5: "\/" ( { h where h is Element of L : h [= f . h } ,L) [= f . ("\/" ( { h where h is Element of L : h [= f . h } ,L)) by A3, LATTICES:7;

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 A5, LATTICES:8; :: according to ABIAN:def 4 :: thesis: verum