theorem Th13: :: ROBBINS3:13

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 join-absorbing holds
L is join-absorbing