let S be Element of CQC-Sub-WFF ; :: thesis: ( (Sub_not S) `1 = 'not' (S `1) & (Sub_not S) `2 = S `2 )
Sub_not S = [('not' (S `1)),(S `2)] by SUBSTUT1:def 20;
hence ( (Sub_not S) `1 = 'not' (S `1) & (Sub_not S) `2 = S `2 ) by MCART_1:7; :: thesis: verum