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 k
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 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;
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 S being Element of QC-Sub-WFF st S₁[S] holds
S₁[ Sub_not S] by Def26;
thus for S being Element of QC-Sub-WFF holds S₁[S] from SUBSTUT1:sch 1(A1, A2, A5, A4, A3); :: thesis: verum