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 )
consider s being object such that
A2: s in A by XBOOLE_0:def 1;
reconsider s0 = s as Element of A by A2;
assume not A is trivial ; :: thesis: not A is T_0
then A <> {s0} ;
then consider t being object such that
A3: t in A and
A4: t <> s0 by ZFMISC_1:35;
reconsider s = s, t = t as Point of Y by A2, A3;
assume A5: A is T_0 ; :: thesis: contradiction
now :: thesis: contradiction
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 A3, A4, A5;
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
A6: ( E is closed & s in E ) and
A7: not t in E ;
A c= E by A1, A2, A6, TEX_4:def 2;
hence contradiction by A3, A7; :: 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
A8: F is closed and
A9: not s in F and
A10: t in F ;
A c= F by A1, A3, A8, A10, TEX_4:def 2;
hence contradiction by A2, A9; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum