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