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 & not x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x
let S be Element of CQC-Sub-WFF ; :: 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
S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x
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 S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x )
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: S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x
A3: CQCSub_All ([S,x],xSQ) = Sub_All ([S,x],xSQ) by A1, Def6;
then A4: (CQCSub_All ([S,x],xSQ)) `1 = All (([S,x] `2),(([S,x] `1) `1)) by A1, Th27;
then A5: (CQCSub_All ([S,x],xSQ)) `1 = All (x,(([S,x] `1) `1)) by MCART_1:7;
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, MCART_1:7;
then A7: bound_in ((CQCSub_All ([S,x],xSQ)) `1) = x by QC_LANG2:8;
(CQCSub_All ([S,x],xSQ)) `2 = xSQ by A1, A3, Th27;
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, MCART_1:7;
hence S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x by A7, A6, SUBSTUT1:def 36; :: thesis: verum