:: deftheorem Def8 defines full POLNOT_2:def 7 :
for T being Polish-language
for V being Polish-language of T holds
( V is full iff ex A being Polish-arity-function of T st V = Polish-WFF-set (T,A) );