:: deftheorem defines StoneR LOPCLSET:def 7 :
for BL being non trivial B_Lattice holds StoneR BL = rng (UFilter BL);