set X = the carrier of (ConPoset (P,P));
set Y = the carrier of P;
defpred S1[ object , object ] means for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h & g = $1 holds
$2 = least_fix_point h;
A1:
for x being object st x in the carrier of (ConPoset (P,P)) holds
ex y being object st
( y in the carrier of P & S1[x,y] )
consider IT being Function of the carrier of (ConPoset (P,P)), the carrier of P such that
A2:
for x being object st x in the carrier of (ConPoset (P,P)) holds
S1[x,IT . x]
from FUNCT_2:sch 1(A1);
for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
IT . g = least_fix_point h
by A2;
hence
ex b1 being Function of (ConPoset (P,P)),P st
for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b1 . g = least_fix_point h
; verum