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