let L be Boolean LATTICE; :: thesis: for x being Element of L holds 'not' (x ~) = 'not' x
let x be Element of L; :: thesis: 'not' (x ~) = 'not' x
for x being Element of L holds 'not' ('not' x) = x by WAYBEL_1:87;
then 'not' x is_a_complement_of x by WAYBEL_1:86;
then ('not' x) ~ is_a_complement_of x ~ by Th35;
hence 'not' (x ~) = 'not' x by YELLOW_5:11; :: thesis: verum