let Al be QC-alphabet ; :: thesis: for S being Element of CQC-Sub-WFF Al holds
( (Sub_not S) `1 = 'not' (S `1) & (Sub_not S) `2 = S `2 )
let S be Element of CQC-Sub-WFF Al; :: 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 ) ; :: thesis: verum