for L being reflexive antisymmetric with_infima RelStr
for a, b being Element of L holds
( a = a "/\" b iff a <= b )