:: deftheorem defines Heyting LATTICE2:def 5 :
for IT being Lattice holds
( IT is Heyting iff ( IT is implicative & IT is lower-bounded ) );