:: deftheorem Def30 defines Sub_the_argument_of SUBSTUT1:def 30 :
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_negative holds
for b₃ being Element of QC-Sub-WFF A holds
( b₃ = Sub_the_argument_of S iff S = Sub_not b₃ );