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 monotone Function of P,Q by Lm17;
for L being non empty Chain of P holds f . (sup L) <= sup (f .: L)

let L be non empty Chain of P; :: thesis:
reconsider M1 = f .: L as non empty Chain of Q by Th1;
set q1 = sup M1;
set a = sup L;
set M = F -image (sup L);
A1: f . (sup L) = sup (F -image (sup L)) by Def10;
for q being Element of Q st q in F -image (sup L) holds
q <= sup M1

let q be Element of Q; :: thesis:
assume q in F -image (sup L) ; :: thesis:
then consider q0 being Element of Q such that
A2: ( q = q0 & ex g being continuous Function of P,Q st
( g in F & q0 = g . (sup L) ) ) ;
consider g being continuous Function of P,Q such that
A3: ( g in F & q0 = g . (sup L) ) by A2;
reconsider M2 = g .: L as non empty Chain of Q by Th1;
A4: q = sup M2 by Th6, A2, A3;
for q2 being Element of Q st q2 in M2 holds
q2 <= sup M1

let q2 be Element of Q; :: thesis:
assume q2 in M2 ; :: thesis:
then consider x being object such that
A5: ( x in dom g & x in L & q2 = g . x ) by FUNCT_1:def 6;
reconsider x = x as Element of P by A5;
set Mx = F -image x;
A6: f . x = sup (F -image x) by Def10;
set y = f . x;
x in the carrier of P ;
then x in dom f by FUNCT_2:def 1;
then f . x in M1 by A5, FUNCT_1:def 6;
then A7: f . x <= sup M1 by Lm18;
q2 in F -image x by A5, A3;
then q2 <= sup (F -image x) by Lm18;
hence q2 <= sup M1 by A7, A6, ORDERS_2:3; :: thesis:

end;

end;

hence f . (sup L) <= sup (f .: L) by A1, Lm19; :: thesis:

end;