theorem Th16: :: SHEFFER1:16

for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr holds L is join-associative