theorem Th38: :: SUBLEMMA:38

for Al being QC-alphabet
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 & 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)) & not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in Bound_Vars (S `1) )