for X being non empty TopSpace
for X0 being non empty SubSpace of X holds
( X0 is maximal_discrete iff ( X0 is discrete & ( for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) )