let P be non empty strict chain-complete Poset; 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));
( 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
;
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;
( 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 )
;
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;
verum
end;
hence
fix_func P is monotone Function of (ConPoset (P,P)),P
by ORDERS_3:def 5; verum