A2: for x being bound_QC-variable
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P₁[S] holds
P₁[ Sub_All ([S,x],xSQ)]

proof

let x be bound_QC-variable; :: thesis: for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P₁[S] holds
P₁[ Sub_All ([S,x],xSQ)]
let S be Element of CQC-Sub-WFF ; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P₁[S] holds
P₁[ Sub_All ([S,x],xSQ)]
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable & P₁[S] implies P₁[ Sub_All ([S,x],xSQ)] )
assume that
A3: [S,x] is quantifiable and
A4: P₁[S] ; :: thesis: P₁[ Sub_All ([S,x],xSQ)]
CQCSub_All ([S,x],xSQ) = Sub_All ([S,x],xSQ) by A3, Def6;
hence P₁[ Sub_All ([S,x],xSQ)] by A1, A3, A4; :: thesis: verum

end;

for S, S9 being Element of CQC-Sub-WFF st S `2 = S9 `2 & P₁[S] & P₁[S9] holds
P₁[ Sub_& (S,S9)]

proof

let S, S9 be Element of CQC-Sub-WFF ; :: thesis: ( S `2 = S9 `2 & P₁[S] & P₁[S9] implies P₁[ Sub_& (S,S9)] )
assume that
A5: S `2 = S9 `2 and
A6: ( P₁[S] & P₁[S9] ) ; :: thesis: P₁[ Sub_& (S,S9)]
CQCSub_& (S,S9) = Sub_& (S,S9) by A5, Def4;
hence P₁[ Sub_& (S,S9)] by A1, A5, A6; :: thesis: verum

end;

then A7: 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
( P₁[ Sub_P (P,ll,e)] & ( S is Sub_VERUM implies P₁[S] ) & ( P₁[S] implies P₁[ Sub_not S] ) & ( S `2 = S9 `2 & P₁[S] & P₁[S9] implies P₁[ Sub_& (S,S9)] ) & ( [S,x] is quantifiable & P₁[S] implies P₁[ Sub_All ([S,x],SQ)] ) ) by A1, A2;
thus for S being Element of CQC-Sub-WFF holds P₁[S] from SUBSTUT1:sch 5(A7); :: thesis: verum