:: deftheorem defines Polish-ext-arity POLNOT_2:def 22 :
for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V holds Polish-ext-arity Q = Polish-ext-arity ((Polish-arity V),Q);