A2: now
let x be bound_QC-variable; :: thesis: for S being Element of QC-Sub-WFF
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All [S,x],SQ]
let S be Element of QC-Sub-WFF ; :: thesis: for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All [S,x],SQ]
let SQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable & P1[S] implies P1[ Sub_All [S,x],SQ] )
assume that
A3: [S,x] is quantifiable and
A4: P1[S] ; :: thesis: P1[ Sub_All [S,x],SQ]
[S,x] `1 = Sub_the_scope_of (Sub_All [S,x],SQ) by A3, Th21;
then A5: S = Sub_the_scope_of (Sub_All [S,x],SQ) by MCART_1:7;
Sub_All [S,x],SQ is Sub_universal by A3, Th14;
hence P1[ Sub_All [S,x],SQ] by A1, A4, A5; :: thesis: verum
end;
A6: now
let S1, S2 be Element of QC-Sub-WFF ; :: thesis: ( S1 `2 = S2 `2 & P1[S1] & P1[S2] implies P1[ Sub_& S1,S2] )
assume that
A7: S1 `2 = S2 `2 and
A8: ( P1[S1] & P1[S2] ) ; :: thesis: P1[ Sub_& S1,S2]
A9: S2 = Sub_the_right_argument_of (Sub_& S1,S2) by A7, Th19;
( Sub_& S1,S2 is Sub_conjunctive & S1 = Sub_the_left_argument_of (Sub_& S1,S2) ) by A7, Th13, Th18;
hence P1[ Sub_& S1,S2] by A1, A8, A9; :: thesis: verum
end;
A10: now
let S be Element of QC-Sub-WFF ; :: thesis: ( P1[S] implies P1[ Sub_not S] )
assume A11: P1[S] ; :: thesis: P1[ Sub_not S]
S = Sub_the_argument_of (Sub_not S) by Def30;
hence P1[ Sub_not S] by A1, A11; :: thesis: verum
end;
A12: for S being Element of QC-Sub-WFF st S is Sub_VERUM holds
P1[S] by A1;
A13: for k being Element of NAT
for P being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds P1[ Sub_P P,ll,e] by A1;
thus for S being Element of QC-Sub-WFF holds P1[S] from SUBSTUT1:sch 1(A13, A12, A10, A6, A2); :: thesis: verum