theorem Th12: :: TEX_1:12

for X being non empty TopSpace st ( for A being Subset of X st A <> the carrier of X holds
Int A = {} ) holds
X is anti-discrete