for S being Element of CQC-Sub-WFF F₁() holds P₁[S]

A1: for S, S9 being Element of CQC-Sub-WFF F₁()
for x being bound_QC-variable of F₁()
for SQ being second_Q_comp of [S,x]
for k being Nat
for ll being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁()
for e being Element of vSUB F₁() holds
( P₁[ Sub_P (P,ll,e)] & ( S is F₁() -Sub_VERUM implies P₁[S] ) & ( P₁[S] implies P₁[ Sub_not S] ) & ( S `2 = S9 `2 & P₁[S] & P₁[S9] implies P₁[ CQCSub_& (S,S9)] ) & ( [S,x] is quantifiable & P₁[S] implies P₁[ CQCSub_All ([S,x],SQ)] ) )