let Y be non empty TopStruct ; :: thesis: for A being non empty Subset of Y st A is anti-discrete & not A is trivial holds
not A is T_0
let A be non empty Subset of Y; :: thesis: ( A is anti-discrete & not A is trivial implies not A is T_0 )
assume A1: A is anti-discrete ; :: thesis: ( A is trivial or not A is T_0 )
assume A2: not A is trivial ; :: thesis: not A is T_0
consider s being set such that
A3: s in A by XBOOLE_0:def 1;
reconsider s0 = s as Element of A by A3;
A <> {s0} by A2;
then consider t being set such that
A4: t in A and
A5: t <> s0 by ZFMISC_1:41;
reconsider s = s, t = t as Point of Y by A3, A4;
assume A6: A is T_0 ; :: thesis: contradiction

now

per cases ( ex E being Subset of Y st
( E is closed & s in E & not t in E ) or ex F being Subset of Y st
( F is closed & not s in F & t in F ) ) by A4, A5, A6, Def9;

suppose ex E being Subset of Y st
( E is closed & s in E & not t in E ) ; :: thesis: contradiction

then consider E being Subset of Y such that
A7: E is closed and
A8: s in E and
A9: not t in E ;
A c= E by A1, A3, A7, A8, TEX_4:def 2;
hence contradiction by A4, A9; :: thesis: verum

end;

suppose ex F being Subset of Y st
( F is closed & not s in F & t in F ) ; :: thesis: contradiction

then consider F being Subset of Y such that
A10: F is closed and
A11: not s in F and
A12: t in F ;
A c= F by A1, A4, A10, A12, TEX_4:def 2;
hence contradiction by A3, A11; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum