let L be complete Lattice; :: thesis: for f being monotone UnOp of L

for x, y being Element of (FixPoints f)

for a, b being Element of L st x = a & y = b holds

( x [= y iff a [= b )

let f be monotone UnOp of L; :: thesis: for x, y being Element of (FixPoints f)

for a, b being Element of L st x = a & y = b holds

( x [= y iff a [= b )

A1: ex P being non empty with_suprema with_infima Subset of L st

( P = { x where x is Element of L : x is_a_fixpoint_of f } & FixPoints f = latt P ) by Def9;

let x, y be Element of (FixPoints f); :: thesis: for a, b being Element of L st x = a & y = b holds

( x [= y iff a [= b )

let a, b be Element of L; :: thesis: ( x = a & y = b implies ( x [= y iff a [= b ) )

assume A2: ( x = a & y = b ) ; :: thesis: ( x [= y iff a [= b )

ex a9, b9 being Element of L st

( x = a9 & y = b9 & ( x [= y implies a9 [= b9 ) & ( a9 [= b9 implies x [= y ) ) by A1, Def8;

hence ( x [= y iff a [= b ) by A2; :: thesis: verum

for x, y being Element of (FixPoints f)

for a, b being Element of L st x = a & y = b holds

( x [= y iff a [= b )

let f be monotone UnOp of L; :: thesis: for x, y being Element of (FixPoints f)

for a, b being Element of L st x = a & y = b holds

( x [= y iff a [= b )

A1: ex P being non empty with_suprema with_infima Subset of L st

( P = { x where x is Element of L : x is_a_fixpoint_of f } & FixPoints f = latt P ) by Def9;

let x, y be Element of (FixPoints f); :: thesis: for a, b being Element of L st x = a & y = b holds

( x [= y iff a [= b )

let a, b be Element of L; :: thesis: ( x = a & y = b implies ( x [= y iff a [= b ) )

assume A2: ( x = a & y = b ) ; :: thesis: ( x [= y iff a [= b )

ex a9, b9 being Element of L st

( x = a9 & y = b9 & ( x [= y implies a9 [= b9 ) & ( a9 [= b9 implies x [= y ) ) by A1, Def8;

hence ( x [= y iff a [= b ) by A2; :: thesis: verum