defpred S₁[ Element of QC-Sub-WFF ] means CQC_Sub $1 is Element of CQC-WFF ;
A1: for S, S9 being Element of CQC-Sub-WFF
for x being bound_QC-variable
for SQ being second_Q_comp of [S,x]
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k
for e being Element of vSUB holds
( S₁[ Sub_P P,ll,e] & ( S is 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 holds S₁[S] from SUBSTUT1:sch 5(A1);
hence CQC_Sub S is Element of CQC-WFF ; :: thesis: verum