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