let L be Stone Lattice; :: thesis: for x being Element of L st x in DenseElements L holds
x * = Bottom L
let x be Element of L; :: thesis: ( x in DenseElements L implies x * = Bottom L )
assume x in DenseElements L ; :: thesis: x * = Bottom L
then consider aa being Element of L such that
A1: ( x = aa & aa * = Bottom L ) ;
thus x * = Bottom L by A1; :: thesis: verum