:: deftheorem defines lfp KNASTER:def 10 :
for L being complete Lattice
for f being monotone UnOp of L holds lfp f = (f,(nextcard the carrier of L)) +. (Bottom L);