let P, Q be non empty strict chain-complete Poset; :: thesis:
let L be non empty Chain of P; :: thesis:
let f be monotone Function of P,Q; :: thesis:
reconsider M = f .: L as non empty Chain of Q by Th1;
set r = sup L;
set u = f . (sup L);
A1: ( ex_sup_of L,P & ex_sup_of M,Q ) by Def1;
for q being Element of Q st q in M holds
q <= f . (sup L)

let q be Element of Q; :: thesis:
assume q in M ; :: thesis:
then consider x being object such that
A2: ( x in dom f & x in L & q = f . x ) by FUNCT_1:def 6;
reconsider x = x as Element of P by A2;
L is_<=_than sup L by A1, YELLOW_0:def 9;
then x <= sup L by A2;
hence q <= f . (sup L) by A2, ORDERS_3:def 5; :: thesis:

end;