:: deftheorem defines StoneBLattice LOPCLSET:def 9 :
for BL being non trivial B_Lattice holds StoneBLattice BL = OpenClosedSetLatt (StoneSpace BL);