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

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