for S, T being antisymmetric with_suprema RelStr
for X, Y being Subset of [:S,T:] holds
( proj1 (X "\/" Y) = (proj1 X) "\/" (proj1 Y) & proj2 (X "\/" Y) = (proj2 X) "\/" (proj2 Y) )