for L being antisymmetric RelStr holds
( L is with_infima iff for a, b being Element of L holds ex_inf_of {a,b},L )