set L = the non empty strict Boolean LATTICE;
take the non empty strict Boolean LATTICE ; :: thesis: ( the non empty strict Boolean LATTICE is strict & the non empty strict Boolean LATTICE is Heyting & not the non empty strict Boolean LATTICE is empty )
thus ( the non empty strict Boolean LATTICE is strict & the non empty strict Boolean LATTICE is Heyting & not the non empty strict Boolean LATTICE is empty ) ; :: thesis: verum