let Al be QC-alphabet ; for p being Element of CQC-WFF Al holds still_not-bound_in p c= Bound_Vars p
defpred S1[ Element of QC-WFF Al] means still_not-bound_in $1 c= Bound_Vars $1;
Bound_Vars (VERUM Al) = {}
by SUBSTUT1:2;
then A1:
for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! l] & ( S1[p] implies S1[ 'not' p] ) & ( S1[p] & S1[q] implies S1[p '&' q] ) & ( S1[p] implies S1[ All (x,p)] ) )
by Th43, Th44, Th45, Th46, QC_LANG3:3;
thus
for p being Element of CQC-WFF Al holds S1[p]
from CQC_LANG:sch 1(A1); verum