let P be non empty strict chain-complete Poset; :: thesis: for p1, p2 being Element of (ConPoset P,P) st p1 <= p2 holds
( p1 in ConFuncs P,P & p2 in ConFuncs P,P & ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 ) )
let p1, p2 be Element of (ConPoset P,P); :: thesis: ( p1 <= p2 implies ( p1 in ConFuncs P,P & p2 in ConFuncs P,P & ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 ) ) )
assume p1 <= p2 ; :: thesis: ( p1 in ConFuncs P,P & p2 in ConFuncs P,P & ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 ) )
then A1: [p1,p2] in ConRelat P,P by ORDERS_2:def 9;
ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 )

proof

consider g1, g2 being Function of P,P such that
B1: ( p1 = g1 & p2 = g2 & g1 <= g2 ) by A1, DefConRelat;
reconsider h1 = p1, h2 = p2 as continuous Function of P,P by LemCastFunc01;
g1 = h1 by B1;
then reconsider g1 = g1 as continuous Function of P,P ;
g2 = h2 by B1;
then reconsider g2 = g2 as continuous Function of P,P ;
take g1 ; :: thesis: ex g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 )
take g2 ; :: thesis: ( p1 = g1 & p2 = g2 & g1 <= g2 )
thus ( p1 = g1 & p2 = g2 & g1 <= g2 ) by B1; :: thesis: verum

end;

hence ( p1 in ConFuncs P,P & p2 in ConFuncs P,P & ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 ) ) ; :: thesis: verum