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