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) by SUBLEMMA:16;
then A1: (Sub_not [p,Sub]) `1 = 'not' p by MCART_1:7;
(Sub_not [p,Sub]) `2 = [p,Sub] `2 by SUBLEMMA:16;
then A2: (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, A2, MCART_1:8; :: thesis: verum