let p be Element of CQC-WFF ; :: thesis: for Sub being CQC_Substitution holds [('not' p),Sub] = Sub_not [p,Sub]
let Sub be CQC_Substitution; :: thesis: [('not' p),Sub] = Sub_not [p,Sub]
set S = [p,Sub];
( (Sub_not [p,Sub]) `1 = 'not' ([p,Sub] `1 ) & (Sub_not [p,Sub]) `2 = [p,Sub] `2 ) by SUBLEMMA:17;
then A1: ( (Sub_not [p,Sub]) `1 = 'not' p & (Sub_not [p,Sub]) `2 = Sub ) by MCART_1:7;
Sub_not [p,Sub] = [('not' ([p,Sub] `1 )),([p,Sub] `2 )] by SUBSTUT1:def 20;
hence [('not' p),Sub] = Sub_not [p,Sub] by A1, MCART_1:8; :: thesis: verum