for L being bounded LATTICE holds
( L is distributive & L is complemented iff ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) )