theorem :: TEX_2:67

for X being non empty discrete TopSpace
for X0 being non empty SubSpace of X holds X0 is_a_retract_of X