set L = the strict B_Lattice;
the strict B_Lattice is I_Lattice ;
hence ex b₁ being Lattice st
( b₁ is Heyting & b₁ is strict ) ; :: thesis: verum