let P, Q be non empty strict chain-complete Poset; :: thesis:
let F be non empty Chain of (ConPoset (P,Q)); :: thesis:
reconsider f = sup_func F as Function of P,Q ;
for p, p1 being Element of P st p <= p1 holds
for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1

let p, p1 be Element of P; :: thesis:
assume A1: p <= p1 ; :: thesis:
for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1

let q, q1 be Element of Q; :: thesis:
assume A2: ( q = f . p & q1 = f . p1 ) ; :: thesis:
reconsider X = F -image p as non empty Chain of Q ;
reconsider X1 = F -image p1 as non empty Chain of Q ;
A3: ( ex_sup_of X,Q & ex_sup_of X1,Q ) by Def1;
A4: q = sup X by A2, Def10;
q1 = sup X1 by A2, Def10;
then A5: X1 is_<=_than q1 by A3, YELLOW_0:def 9;
for x being Element of Q st x in X holds
x <= q1

let x be Element of Q; :: thesis:
assume x in X ; :: thesis:
then consider a being Element of Q such that
A6: ( x = a & ex g being continuous Function of P,Q st
( g in F & a = g . p ) ) ;
consider g being continuous Function of P,Q such that
A7: ( g in F & a = g . p ) by A6;
reconsider b = g . p1 as Element of Q ;
A8: a <= b by A1, A7, ORDERS_3:def 5;
b in X1 by A7;
then b <= q1 by A5;
hence x <= q1 by A6, A8, ORDERS_2:3; :: thesis:

end;

end;

hence for q, q1 being Element of Q st q = f . p & q1 = f . p1 holds
q <= q1 ; :: thesis:

end;