theorem :: TEX_3:7

for X being non trivial TopSpace
for D being non empty proper Subset of X ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0