let L1, L2 be non empty antisymmetric RelStr ; :: thesis: for D being Subset of [:L1,L2:] st ex_sup_of D,[:L1,L2:] holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]
let D be Subset of [:L1,L2:]; :: thesis: ( ex_sup_of D,[:L1,L2:] implies sup D = [(sup (proj1 D)),(sup (proj2 D))] )
assume A1: ex_sup_of D,[:L1,L2:] ; :: thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]

per cases ( D <> {} or D = {} ) ;

suppose D <> {} ; :: thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]

hence sup D = [(sup (proj1 D)),(sup (proj2 D))] by A1, YELLOW_3:46; :: thesis: verum

end;

suppose D = {} ; :: thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]

then ( ex_sup_of {} ,L1 & ex_sup_of {} ,L2 ) by A1, FUNCT_5:10, YELLOW_3:41;
then ( L1 is lower-bounded & L2 is lower-bounded ) by Th6;
hence sup D = [(sup (proj1 D)),(sup (proj2 D))] by A1, YELLOW10:5; :: thesis: verum

end;

end;