:: deftheorem defines closed QC_LANG1:def 31 :
for A being QC-alphabet
for p being QC-formula of A holds
( p is closed iff still_not-bound_in p = {} );