let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for Sub being CQC_Substitution
for S being Element of CQC-Sub-WFF st S `2 = (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub])) & S `1 = p holds
( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF st S1 = [(All x,p),Sub] )
let x be bound_QC-variable; :: thesis: for Sub being CQC_Substitution
for S being Element of CQC-Sub-WFF st S `2 = (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub])) & S `1 = p holds
( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF st S1 = [(All x,p),Sub] )
let Sub be CQC_Substitution; :: thesis: for S being Element of CQC-Sub-WFF st S `2 = (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub])) & S `1 = p holds
( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF st S1 = [(All x,p),Sub] )
let S be Element of CQC-Sub-WFF ; :: thesis: ( S `2 = (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub])) & S `1 = p implies ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF st S1 = [(All x,p),Sub] ) )
set Sub1 = (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub]));
reconsider Sub = Sub as CQC_Substitution ;
assume that
A1: S `2 = (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub])) and
A2: S `1 = p ; :: thesis: ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF st S1 = [(All x,p),Sub] )
A3: ( [S,x] `2 = x & ([S,x] `1 ) `1 = p ) by A2, MCART_1:7;
A4: ( the_scope_of (All x,p) = p & All x,p is universal ) by QC_LANG1:def 20, QC_LANG2:8;
( (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub])) = ExpandSub x,p,(RestrictSub x,(All x,p),Sub) & bound_in (All x,p) = x ) by Th9, QC_LANG2:8;
then All x,p,Sub PQSub (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub])) by A4, SUBSTUT1:def 14;
then consider a being set such that
A5: a = [[(All x,p),Sub],((@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub])))] and
A6: All x,p,Sub PQSub (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub])) ;
a in QSub by A5, A6, SUBSTUT1:def 15;
then A7: QSub . [(All x,p),Sub] = (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub])) by A5, FUNCT_1:8;
A8: ([S,x] `1 ) `2 = (@ (RestrictSub x,(All x,p),Sub)) +* (x | (S_Bound [(All x,p),Sub])) by A1, MCART_1:7;
hence [S,x] is quantifiable by A7, A3, SUBSTUT1:def 22; :: thesis: ex S1 being Element of CQC-Sub-WFF st S1 = [(All x,p),Sub]
A9: [S,x] is quantifiable by A7, A8, A3, SUBSTUT1:def 22;
then reconsider Sub = Sub as second_Q_comp of [S,x] by A7, A8, A3, SUBSTUT1:def 23;
take S1 = CQCSub_All [S,x],Sub; :: thesis: S1 = [(All x,p),Sub]
S1 = Sub_All [S,x],Sub by A9, SUBLEMMA:def 6;
hence S1 = [(All x,p),Sub] by A3, A9, SUBSTUT1:def 24; :: thesis: verum