let L be Stone Lattice; :: thesis: Top L in DenseElements L
(Top L) * = Bottom L by Th11a;
hence Top L in DenseElements L ; :: thesis: verum