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