:: deftheorem defines NBI CQC_SIM1:def 9 :
for A being QC-alphabet
for p being Element of CQC-WFF A holds NBI p = { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p } ;