let L be non empty antisymmetric RelStr ; :: thesis: for X being Subset of [:L,L:] st X c= id the carrier of L & ex_sup_of X,[:L,L:] holds
sup X in id the carrier of L
let X be Subset of [:L,L:]; :: thesis: ( X c= id the carrier of L & ex_sup_of X,[:L,L:] implies sup X in id the carrier of L )
assume ( X c= id the carrier of L & ex_sup_of X,[:L,L:] ) ; :: thesis: sup X in id the carrier of L
then ( sup X = [(sup (proj1 X)),(sup (proj2 X))] & sup (proj1 X) = sup (proj2 X) ) by Th1, Th8;
hence sup X in id the carrier of L by RELAT_1:def 10; :: thesis: verum