for A being QC-alphabet
for s being QC-formula of A
for x, y being bound_QC-variable of A holds
( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) )