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 5;
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
A2: ( p1 = g1 & p2 = g2 & g1 <= g2 ) by A1, Def7;
reconsider h1 = p1, h2 = p2 as continuous Function of P,P by Lm24;
g1 = h1 by A2;
then reconsider g1 = g1 as continuous Function of P,P ;
g2 = h2 by A2;
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 A2; :: 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