theorem :: ROBBINS3:17

for L1, L2 being non empty /\-SemiLattStr st /\-SemiLattStr(# the carrier of L1, the L_meet of L1 #) = /\-SemiLattStr(# the carrier of L2, the L_meet 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 ;