for Y being non empty TopStruct
for A being non empty Subset of Y st A is anti-discrete & not A is trivial holds
not A is T_0