consider L being strict B_Lattice;
( L is 0_Lattice & L is I_Lattice ) by FILTER_0:40;
then L is H_Lattice ;
hence ex b₁ being Lattice st
( b₁ is Heyting & b₁ is strict ) ; :: thesis: verum