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