for L being transitive antisymmetric with_suprema RelStr
for a, b being Element of L
for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds
a "\/" b is_<=_than A "\/" B