theorem Th4: :: SHEFFER1:4

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' LattStr
for x being Element of L holds x "\/" (Top' L) = Top' L