:: deftheorem Def26 defines Sub_negative SUBSTUT1:def 26 :
for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is Sub_negative iff ex S9 being Element of QC-Sub-WFF A st S = Sub_not S9 );