:: deftheorem defines Sub_not SUBSTUT1:def 20 :
for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds Sub_not S = [('not' (S `1)),(S `2)];