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