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