theorem Th67: :: POLNOT_1:67

for T being Polish-language
for A being Polish-arity-function of T
for F being Polish-WFF of T,A holds T -tail F in (Polish-WFF-set (T,A)) ^^ (Polish-arity F)