theorem Th13: :: TSP_1:13

for Y being non empty TopStruct
for Y0 being non empty SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is T_0 iff Y0 is V142() ) ;