consider L being B_Lattice;
take L ; :: thesis: L is Heyting
thus ( L is implicative & L is lower-bounded ) by FILTER_0:40; :: according to LATTICE2:def 6 :: thesis: verum