for L being bounded LATTICE st L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) holds
for x being Element of L holds 'not' x is_a_complement_of x