theorem :: POLNOT_2:15

for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V holds V c= Q