:: deftheorem defines Heyting WAYBEL_1:def 19 :
for H being non empty RelStr holds
( H is Heyting iff ( H is LATTICE & ( for x being Element of H holds x "/\" is lower_adjoint ) ) );