theorem Th18: :: SHEFFER1:18

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds Top L = Top' L