theorem :: POLNOT_2:16

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 st Polish-ext-head F in T holds
Polish-ext-head F = T -head F by Th10;