for L being reflexive antisymmetric with_suprema RelStr
for a being Element of L holds a "\/" a = a