let L be non empty reflexive antisymmetric RelStr ; :: thesis: ( L is /\-complete implies L is with_infima )
assume L is /\-complete ; :: thesis: L is with_infima
then for a, b being Element of L holds ex_inf_of {a,b},L by Th76;
hence L is with_infima by YELLOW_0:21; :: thesis: verum