let P, Q be non empty chain-complete Poset; :: thesis:
let L be Chain of [:P,Q:]; :: thesis:
set R = the InternalRel of [:P,Q:];
assume not L is empty ; :: thesis:
then reconsider L = L as non empty Chain of [:P,Q:] ;
reconsider L1 = proj1 L as non empty Chain of P ;
reconsider L2 = proj2 L as non empty Chain of Q ;
reconsider z = [(sup L1),(sup L2)] as Element of [:P,Q:] ;
a1: for x being Element of [:P,Q:] st x in L holds
x <= z

end;

let y be Element of [:P,Q:]; :: thesis:
consider p1 being Element of P, q1 being Element of Q such that
B1: y = [p1,q1] by ThProdPoset01;
( L is_<=_than y implies z <= y )

let p be Element of P; :: thesis:
assume p in L1 ; :: thesis:
then consider q0 being object such that
D1: [p,q0] in L by XTUPLE_0:def 12;
q0 in L2 by D1, XTUPLE_0:def 13;
then reconsider q0 = q0 as Element of Q ;
reconsider b = [p,q0] as Element of [:P,Q:] ;
b <= y by C1, D1;
hence p <= p1 by B1, YELLOW_3:11; :: thesis:

end;

for q being Element of Q st q in L2 holds
q <= q1

let q be Element of Q; :: thesis:
assume q in L2 ; :: thesis:
then consider p0 being object such that
D1: [p0,q] in L by XTUPLE_0:def 13;
p0 in L1 by D1, XTUPLE_0:def 12;
then reconsider p0 = p0 as Element of P ;
reconsider b = [p0,q] as Element of [:P,Q:] ;
b <= y by C1, D1;
hence q <= q1 by B1, YELLOW_3:11; :: thesis:

end;

end;

hence ( L is_<=_than y implies z <= y ) ; :: thesis:

end;