defpred S₁[ Element of QC-Sub-WFF ] means ( $1 is Sub_VERUM or $1 is Sub_atomic or $1 is Sub_negative or $1 is Sub_conjunctive or $1 is Sub_universal );
A1: for k being Element of NAT
for p being QC-pred_symbol of k
for ll being QC-variable_list of
for e being Element of vSUB holds S₁[ Sub_P p,ll,e] ;
A2: for S being Element of QC-Sub-WFF st S is Sub_VERUM holds
S₁[S] ;
A3: for S being Element of QC-Sub-WFF st S₁[S] holds
S₁[ Sub_not S] by Def26;
A4: for S1, S2 being Element of QC-Sub-WFF st S1 `2 = S2 `2 & S₁[S1] & S₁[S2] holds
S₁[ Sub_& S1,S2] by Def27;
A5: for x being bound_QC-variable
for S being Element of QC-Sub-WFF
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S₁[S] holds
S₁[ Sub_All [S,x],SQ] by Def28;
thus for S being Element of QC-Sub-WFF holds S₁[S] from SUBSTUT1:sch 1(A1, A2, A3, A4, A5); :: thesis: verum