for L being RelStr
for X, Y being set st X c= Y & ex_sup_of X,L & ex_sup_of Y,L holds
"\/" (X,L) <= "\/" (Y,L)