A2: for S, S' being Element of CQC-Sub-WFF st S `2 = S' `2 & P₁[S] & P₁[S'] holds
P₁[ Sub_& S,S']

proof

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

end;

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 A4: ( [S,x] is quantifiable & P₁[S] ) ; :: thesis: P₁[ Sub_All [S,x],xSQ]
then CQCSub_All [S,x],xSQ = Sub_All [S,x],xSQ by Def6;
hence P₁[ Sub_All [S,x],xSQ] by A1, A4; :: thesis: verum

end;

then A5: for S, S' 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
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 = S' `2 & P₁[S] & P₁[S'] implies P₁[ Sub_& S,S'] ) & ( [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(A5); :: thesis: verum