defpred S₁[ Element of QC-Sub-WFF A] means CQC_Sub $1 is Element of CQC-WFF A;
A1: for S, S9 being Element of CQC-Sub-WFF A
for x being bound_QC-variable of A
for SQ being second_Q_comp of [S,x]
for k being Nat
for ll being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A
for e being Element of vSUB A holds
( S₁[ Sub_P (P,ll,e)] & ( S is A -Sub_VERUM implies S₁[S] ) & ( S₁[S] implies S₁[ Sub_not S] ) & ( S `2 = S9 `2 & S₁[S] & S₁[S9] implies S₁[ Sub_& (S,S9)] ) & ( [S,x] is quantifiable & S₁[S] implies S₁[ Sub_All ([S,x],SQ)] ) ) by Th33, Th35, Th36, Th37, Th38;
for S being Element of CQC-Sub-WFF A holds S₁[S] from SUBSTUT1:sch 5(A1);
hence CQC_Sub S is Element of CQC-WFF A ; :: thesis: verum