let S, T be non empty antisymmetric lower-bounded RelStr ; 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:]; ( ( [: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:] )
; sup D = [(sup (proj1 D)),(sup (proj2 D))]