let P, Q be non empty chain-complete Poset; :: thesis: for L being Chain of [:P,Q:] st not L is empty holds
ex_sup_of L,[:P,Q:]
let L be Chain of [:P,Q:]; :: thesis: ( not L is empty implies ex_sup_of L,[:P,Q:] )
set R = the InternalRel of [:P,Q:];
assume not L is empty ; :: thesis: ex_sup_of L,[:P,Q:]
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

proof

let x be Element of [:P,Q:]; :: thesis: ( x in L implies x <= z )
assume B1: x in L ; :: thesis: x <= z
consider p being Element of P, q being Element of Q such that
B2: x = [p,q] by ThProdPoset01;
( p in L1 & q in L2 ) by XTUPLE_0:def 12, XTUPLE_0:def 13, B1, B2;
then ( p <= sup L1 & q <= sup L2 ) by Thsup01;
hence x <= z by YELLOW_3:11, B2; :: thesis: verum

end;

for y being Element of [:P,Q:] st L is_<=_than y holds
z <= y

proof

let y be Element of [:P,Q:]; :: thesis: ( L is_<=_than y implies z <= y )
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 )

proof

assume C1: L is_<=_than y ; :: thesis: z <= y
C2: for p being Element of P st p in L1 holds
p <= p1

proof

let p be Element of P; :: thesis: ( p in L1 implies p <= p1 )
assume p in L1 ; :: thesis: p <= p1
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: verum

end;

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

proof

let q be Element of Q; :: thesis: ( q in L2 implies q <= q1 )
assume q in L2 ; :: thesis: q <= q1
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: verum

end;

then ( sup L1 <= p1 & sup L2 <= q1 ) by C2, Thsup02;
hence z <= y by YELLOW_3:11, B1; :: thesis: verum

end;

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

end;

hence ex_sup_of L,[:P,Q:] by a1, YELLOW_0:15, LATTICE3:def 9; :: thesis: verum