let Q be Quantum_Mechanics; :: thesis: for p being Element of Prop Q holds 'not' ('not' p) = p
let p be Element of Prop Q; :: thesis: 'not' ('not' p) = p
thus 'not' ('not' p) = [(p `1 ),((('not' p) `2 ) ` )] by MCART_1:7
.= [(p `1 ),(((p `2 ) ` ) ` )] by MCART_1:7
.= p by MCART_1:23 ; :: thesis: verum