theorem Th2: :: SUBSTUT1:2

for A being QC-alphabet holds Bound_Vars (VERUM A) = {}