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 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 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 implies not S_Bound (@ (CQCSub_All [S,x],xSQ)) in rng (RestrictSub x,(All x,(S `1 )),xSQ) )
assume A1: [S,x] is quantifiable ; :: thesis: not S_Bound (@ (CQCSub_All [S,x],xSQ)) in rng (RestrictSub x,(All x,(S `1 )),xSQ)
then ( 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) ) by Th39;
hence not S_Bound (@ (CQCSub_All [S,x],xSQ)) in rng (RestrictSub x,(All x,(S `1 )),xSQ) by A1, Th40; :: thesis: verum