for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al) st X c= Y holds
still_not-bound_in X c= still_not-bound_in Y