consider L being non empty strict Boolean LATTICE;
take L ; :: thesis: ( L is strict & L is Heyting & not L is empty )
thus ( L is strict & L is Heyting & not L is empty ) ; :: thesis: verum