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

hereby :: thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) implies ( L is distributive & L is complemented ) )

assume ( L is distributive & L is complemented ) ; :: thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) )
then for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) by Lm6;
hence ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) by Lm7; :: thesis: verum

end;

assume that
A1: L is Heyting and
A2: for x being Element of L holds 'not' ('not' x) = x ; :: thesis: ( L is distributive & L is complemented )
thus L is distributive by A1; :: thesis: L is complemented
let x be Element of L; :: according to WAYBEL_1:def 24 :: thesis: ex y being Element of L st y is_a_complement_of x
take 'not' x ; :: thesis: 'not' x is_a_complement_of x
thus 'not' x is_a_complement_of x by A1, A2, Th86; :: thesis: verum