reconsider f = <:f1,f2:> as monotone Function of P,[:Q1,Q2:] by YELLOW_3:def 2;
for L being non empty Chain of P holds f . (sup L) <= sup (f .: L)

let L be non empty Chain of P; :: thesis:
B0: ( f1 . (sup L) = sup (f1 .: L) & f2 . (sup L) = sup (f2 .: L) ) by POSET_1:6;
AA: dom f = the carrier of P by FUNCT_2:def 1;
then B1: f . (sup L) = [(sup (f1 .: L)),(sup (f2 .: L))] by FUNCT_3:def 7, B0;
reconsider M = f .: L as non empty Chain of [:Q1,Q2:] by POSET_1:1;
B2: sup (f .: L) = [(sup (proj1 M)),(sup (proj2 M))] by YELLOW_3:46, LemProdPoset06;
B3: sup (f1 .: L) <= sup (proj1 M)

reconsider M1 = f1 .: L as non empty Chain of Q1 by POSET_1:1;
set q1 = sup (proj1 M);
for q being Element of Q1 st q in M1 holds
q <= sup (proj1 M)

let q be Element of Q1; :: thesis:
assume q in M1 ; :: thesis:
then consider p being Element of P such that
C1: ( p in L & q = f1 . p ) by FUNCT_2:65;
reconsider a = f2 . p as Element of Q2 ;
f . p = [q,a] by C1, FUNCT_3:def 7, AA;
then [q,a] in M by C1, FUNCT_2:35;
then q in proj1 M by XTUPLE_0:def 12;
hence q <= sup (proj1 M) by Thsup01; :: thesis:

end;

end;

sup (f2 .: L) <= sup (proj2 M)

reconsider M2 = f2 .: L as non empty Chain of Q2 by POSET_1:1;
set q2 = sup (proj2 M);
for q being Element of Q2 st q in M2 holds
q <= sup (proj2 M)

let q be Element of Q2; :: thesis:
assume q in M2 ; :: thesis:
then consider p being Element of P such that
C1: ( p in L & q = f2 . p ) by FUNCT_2:65;
reconsider a = f1 . p as Element of Q1 ;
f . p = [a,q] by C1, FUNCT_3:def 7, AA;
then [a,q] in M by C1, FUNCT_2:35;
then q in proj2 M by XTUPLE_0:def 13;
hence q <= sup (proj2 M) by Thsup01; :: thesis:

end;

end;

end;