theorem :: SUBSTUT1:16

for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds Sub_the_argument_of (Sub_not S) = S by Def30;