:: deftheorem Def1 defines Polish-arity-like POLNOT_2:def 1 :
for F being Function holds
( F is Polish-arity-like iff ex T being Polish-language st F is Polish-arity-function of T );