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