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
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 ; :: 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, 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 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