theorem Th57: :: TEX_2:57

for X being non empty almost_discrete TopSpace
for A being Subset of X st A is maximal_discrete holds
union { (Cl {a}) where a is Point of X : a in A } = the carrier of X