theorem :: ROBBINS3:16

for L1, L2 being non empty \/-SemiLattStr st \/-SemiLattStr(# the carrier of L1, the L_join of L1 #) = \/-SemiLattStr(# the carrier of L2, the L_join of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
a1 "\/" b1 = a2 "\/" b2 ;