theorem :: POLNOT_2:14

for T being Polish-language
for U being b₁ -extending Polish-language
for V being full Polish-language of T
for W being full Polish-language of U holds
( V c= W iff W is -closed )