set L = the B_Lattice;
take the B_Lattice ; :: thesis: the B_Lattice is Heyting
thus ( the B_Lattice is implicative & the B_Lattice is lower-bounded ) ; :: according to LATTICE2:def 5 :: thesis: verum