theorem Th9: :: YELLOW12:9

for L1 being 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