theorem :: POLNOT_2:5

for T being Polish-language holds T is full Polish-language of T