:: deftheorem Def5 defines still_not-bound_in CALCUL_1:def 5 :
for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al
for b₃ being Subset of (bound_QC-variables Al) holds
( b₃ = still_not-bound_in f iff for a being object holds
( a in b₃ iff ex i being Nat ex p being Element of CQC-WFF Al st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) );