theorem Th12: :: ROBBINS3:12

for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-associative holds
L is meet-associative