:: deftheorem defines gfp KNASTER:def 11 :
for L being complete Lattice
for f being monotone UnOp of L holds gfp f = (f,(nextcard the carrier of L)) -. (Top L);