:: deftheorem defines -Sub_VERUM SUBSTUT1:def 19 :
for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is A -Sub_VERUM iff ex e being Element of vSUB A st S = [(VERUM A),e] );