theorem Th38:
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) )