:: deftheorem defines -extending POLNOT_2:def 19 :
for T being Polish-language
for U being b₁ -extending Polish-language
for V being full Polish-language of T
for W being full Polish-language of U holds
( W is V -extending iff Polish-arity V c= Polish-arity W );