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 )
consider P being non empty with_suprema with_infima Subset of L such that
A1: ( P = { x where x is Element of L : x is_a_fixpoint_of f } & FixPoints f = latt P ) by Def11;
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 )
consider a', b' being Element of L such that
A3: ( x = a' & y = b' & ( x [= y implies a' [= b' ) & ( a' [= b' implies x [= y ) ) by A1, Def10;
thus ( x [= y iff a [= b ) by A2, A3; :: thesis: verum