let P be non empty strict chain-complete Poset; :: thesis: fix_func P is monotone Function of (ConPoset (P,P)),P
set IT = fix_func P;
for p1, p2 being Element of (ConPoset (P,P)) st p1 <= p2 holds
for a, b being Element of P st a = (fix_func P) . p1 & b = (fix_func P) . p2 holds
a <= b

proof

let p1, p2 be Element of (ConPoset (P,P)); :: thesis: ( p1 <= p2 implies for a, b being Element of P st a = (fix_func P) . p1 & b = (fix_func P) . p2 holds
a <= b )
assume A1: p1 <= p2 ; :: thesis: for a, b being Element of P st a = (fix_func P) . p1 & b = (fix_func P) . p2 holds
a <= b
let a, b be Element of P; :: thesis: ( a = (fix_func P) . p1 & b = (fix_func P) . p2 implies a <= b )
assume A2: ( a = (fix_func P) . p1 & b = (fix_func P) . p2 ) ; :: thesis: a <= b
consider g1, g2 being continuous Function of P,P such that
A3: ( p1 = g1 & p2 = g2 & g1 <= g2 ) by A1, Lm26;
( a = least_fix_point g1 & b = least_fix_point g2 ) by A2, Def12, A3;
hence a <= b by A3, Th10; :: thesis: verum

end;

hence fix_func P is monotone Function of (ConPoset (P,P)),P by ORDERS_3:def 5; :: thesis: verum