defpred S₁[ Element of QC-WFF ] means still_not-bound_in $1 c= Bound_Vars $1;
A1: for p, q being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! l] & ( S₁[p] implies S₁[ 'not' p] ) & ( S₁[p] & S₁[q] implies S₁[p '&' q] ) & ( S₁[p] implies S₁[ All (x,p)] ) ) by Th44, Th45, Th46, Th47, QC_LANG3:3, SUBSTUT1:2;
thus for p being Element of CQC-WFF holds S₁[p] from CQC_LANG:sch 1(A1); :: thesis: verum