for L being with_suprema Poset
for X, Y being Subset of L
for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds
X "\/" Y = X9 "/\" Y9