set L = the Boolean Lattice;
take the Boolean Lattice ; :: thesis: ( the Boolean Lattice is satisfying_Stone_identity & the Boolean Lattice is pseudocomplemented & the Boolean Lattice is Boolean )
thus ( the Boolean Lattice is satisfying_Stone_identity & the Boolean Lattice is pseudocomplemented & the Boolean Lattice is Boolean ) ; :: thesis: verum