theorem Th1: :: SUBSTUT2:1

for Al being QC-alphabet
for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = VERUM Al & S `2 = Sub )