let L be non empty RelStr ; :: thesis: ( ( for A being Subset of L holds ex_inf_of A,L ) implies L is complete )
assume for A being Subset of L holds ex_inf_of A,L ; :: thesis: L is complete
then for X being set holds ex_inf_of X,L by Th26;
hence L is complete by Th25; :: thesis: verum