theorem Th4: :: ROBBINS3:4
for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
( L is meet-associative & L is join-associative )