:: deftheorem defines DenseLatt LATSTONE:def 11 :
for L being Stone Lattice holds DenseLatt L = latt (L,(DenseElements L));