for A being QC-alphabet
for s being QC-formula of A
for x, y being bound_QC-variable of A holds
( not x in still_not-bound_in (All (x,y,s)) & not y in still_not-bound_in (All (x,y,s)) )