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 that
A1: X c= id the carrier of L and
A2: ex_sup_of X,[:L,L:] ; :: thesis: sup X in id the carrier of L
A3: sup X = [(sup (proj1 X)),(sup (proj2 X))] by A2, Th8;
sup (proj1 X) = sup (proj2 X) by A1, Th1;
hence sup X in id the carrier of L by A3, RELAT_1:def 10; :: thesis: verum