for L being non empty RelStr
for X, Y being set st ( for x being Element of L holds
( x is_>=_than X iff x is_>=_than Y ) ) & ex_sup_of X,L holds
ex_sup_of Y,L