let S, T be non empty antisymmetric lower-bounded RelStr ; :: thesis: for D being Subset of [:S,T:] st ( [:S,T:] is complete or ex_sup_of D,[:S,T:] ) holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]
let D be Subset of [:S,T:]; :: thesis: ( ( [:S,T:] is complete or ex_sup_of D,[:S,T:] ) implies sup D = [(sup (proj1 D)),(sup (proj2 D))] )
assume A1: ( [:S,T:] is complete or ex_sup_of D,[:S,T:] ) ; :: 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 A2: D = {} ; :: thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]

then A3: sup (proj2 D) = Bottom T ;
( sup D = Bottom [:S,T:] & sup (proj1 D) = Bottom S ) by A2;
hence sup D = [(sup (proj1 D)),(sup (proj2 D))] by A3, Th4; :: thesis: verum

end;

end;