for L1 being sup-Semilattice
for L2 being non empty RelStr
for x, y being Element of L1
for x1, y1 being Element 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