reconsider f = fix_func P as monotone Function of (ConPoset (P,P)),P by Lm27;
for L being non empty Chain of (ConPoset (P,P)) holds f . (sup L) <= sup (f .: L) by Lm36;
hence fix_func P is continuous by Th8; :: thesis: verum