:: deftheorem defines Stone LATSTONE:def 6 :
for L being Lattice holds
( L is Stone iff ( L is pseudocomplemented & L is distributive & L is bounded & L is satisfying_Stone_identity ) );