for L being non empty reflexive antisymmetric RelStr holds
( L is /\-complete iff for X being non empty Subset of L holds ex_inf_of X,L )