for V being antisymmetric with_suprema RelStr
for u1, u2 being Element of V holds u1 "\/" u2 = u2 "\/" u1