let L be non empty RelStr ; :: thesis: ( ( for X being set holds ex_inf_of X,L ) implies L is complete )
assume for X being set holds ex_inf_of X,L ; :: thesis: L is complete
then for X being set holds ex_sup_of X,L by Th23;
hence L is complete by Th24; :: thesis: verum