:: deftheorem defines Polish-ext-head POLNOT_2:def 23 :
for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V
for F being Formula of Q holds Polish-ext-head F = (Polish-ext-domain Q) -head F;