let Al be QC-alphabet ; :: thesis: for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & not x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ))
let x be bound_QC-variable of Al; :: thesis: for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & not x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ))
let S be Element of CQC-Sub-WFF Al; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & not x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ))
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable & not x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) implies not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) )
set S1 = CQCSub_All ([S,x],xSQ);
assume that
A1: [S,x] is quantifiable and
A2: not x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) ; :: thesis: not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ))
A3: CQCSub_All ([S,x],xSQ) = Sub_All ([S,x],xSQ) by A1, Def5;
then A4: (CQCSub_All ([S,x],xSQ)) `1 = All (([S,x] `2),(([S,x] `1) `1)) by A1, Th26;
then A5: (CQCSub_All ([S,x],xSQ)) `1 = All (x,(([S,x] `1) `1)) ;
set finSub = RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2));
A6: CQCSub_All ([S,x],xSQ) = @ (CQCSub_All ([S,x],xSQ)) by SUBSTUT1:def 35;
(CQCSub_All ([S,x],xSQ)) `1 = All (x,(([S,x] `1) `1)) by A4;
then A7: bound_in ((CQCSub_All ([S,x],xSQ)) `1) = x by QC_LANG2:7;
(CQCSub_All ([S,x],xSQ)) `2 = xSQ by A1, A3, Th26;
then not bound_in ((CQCSub_All ([S,x],xSQ)) `1) in rng (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))) by A2, A7, A5;
hence not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) by A2, A7, A6, SUBSTUT1:def 36; :: thesis: verum