for L being non empty transitive antisymmetric complete RelStr
for A being Subset of L
for B being non empty Subset of L holds A is_<=_than sup (A "\/" B)