for L being transitive antisymmetric with_suprema RelStr
for x, y, z being Element of L st x <= y holds
x "\/" z <= y "\/" z