for L being complete Lattice
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 )