for L1 being sup-Semilattice
for L2 being non empty RelStr
for X, Y being Subset of L1
for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 holds
X "\/" Y = X1 "\/" Y1