let L be bounded LATTICE; :: thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) implies for x being Element of L holds 'not' x is_a_complement_of x )
assume that
A1: L is Heyting and
A2: for x being Element of L holds 'not' ('not' x) = x ; :: thesis: for x being Element of L holds 'not' x is_a_complement_of x
let x be Element of L; :: thesis: 'not' x is_a_complement_of x
A3: 'not' (x "\/" ('not' x)) = ('not' x) "/\" ('not' ('not' x)) by A1, Th78
.= x "/\" ('not' x) by A2 ;
A4: 'not' x >= 'not' x by ORDERS_2:1;
then x "/\" ('not' x) = Bottom L by A1, Th82;
hence x "\/" ('not' x) = 'not' (Bottom L) by A2, A3
.= Top L by A1, Th80 ;
:: according to WAYBEL_1:def 23 :: thesis: x "/\" ('not' x) = Bottom L
thus x "/\" ('not' x) = Bottom L by A1, A4, Th82; :: thesis: verum