theorem Th45: :: TEX_2:45

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