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 A1: ( [S,x] is quantifiable & not x in rng (RestrictSub x,(All x,(S `1 )),xSQ) ) ; :: thesis: S_Bound (@ (CQCSub_All [S,x],xSQ)) = x
then CQCSub_All [S,x],xSQ = Sub_All [S,x],xSQ by Def6;
then A2: ( (CQCSub_All [S,x],xSQ) `1 = All ([S,x] `2 ),(([S,x] `1 ) `1 ) & (CQCSub_All [S,x],xSQ) `2 = xSQ ) by A1, Th27;
then (CQCSub_All [S,x],xSQ) `1 = All x,(([S,x] `1 ) `1 ) by MCART_1:7;
then A3: bound_in ((CQCSub_All [S,x],xSQ) `1 ) = x by QC_LANG2:8;
set finSub = RestrictSub (bound_in ((CQCSub_All [S,x],xSQ) `1 )),((CQCSub_All [S,x],xSQ) `1 ),((CQCSub_All [S,x],xSQ) `2 );
(CQCSub_All [S,x],xSQ) `1 = All x,(([S,x] `1 ) `1 ) by A2, MCART_1:7;
then A4: 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 A1, A2, A3, MCART_1:7;
@ (CQCSub_All [S,x],xSQ) = CQCSub_All [S,x],xSQ by SUBSTUT1:def 35;
hence S_Bound (@ (CQCSub_All [S,x],xSQ)) = x by A3, A4, SUBSTUT1:def 36; :: thesis: verum