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