:: deftheorem defines -tail POLNOT_1:def 37 :
for T being Polish-language
for A being Polish-arity-function of T
for F being Polish-WFF of T,A holds (T,A) -tail F = T -tail F;