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

A1: for k being Nat
for P being QC-pred_symbol of k,F₁()
for ll being QC-variable_list of k,F₁()
for e being Element of vSUB F₁() holds P₁[ Sub_P (P,ll,e)] and
A2: for S being Element of QC-Sub-WFF F₁() st S is F₁() -Sub_VERUM holds
P₁[S] and
A3: for S being Element of QC-Sub-WFF F₁() st P₁[S] holds
P₁[ Sub_not S] and
A4: for S, S9 being Element of QC-Sub-WFF F₁() st S `2 = S9 `2 & P₁[S] & P₁[S9] holds
P₁[ Sub_& (S,S9)] and
A5: for x being bound_QC-variable of F₁()
for S being Element of QC-Sub-WFF F₁()
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P₁[S] holds
P₁[ Sub_All ([S,x],SQ)]