let A be QC-alphabet ; :: thesis: for S being Element of QC-Sub-WFF A holds
( S is A -Sub_VERUM or S is Sub_atomic or S is Sub_negative or S is Sub_conjunctive or S is Sub_universal )
defpred S₁[ Element of QC-Sub-WFF A] means ( $1 is A -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 Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds S₁[ Sub_P (p,ll,e)] ;
A2: for S being Element of QC-Sub-WFF A st S is A -Sub_VERUM holds
S₁[S] ;
A3: for x being bound_QC-variable of A
for S being Element of QC-Sub-WFF A
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 A 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 A st S₁[S] holds
S₁[ Sub_not S] by Def26;
thus for S being Element of QC-Sub-WFF A holds S₁[S] from SUBSTUT1:sch 1(A1, A2, A5, A4, A3); :: thesis: verum