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