for L being transitive antisymmetric with_suprema RelStr
for X, Y being set st ex_sup_of X,L & ex_sup_of Y,L holds
( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) )