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

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: contradictionend;

hence
contradiction
; :: thesis: verumper 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;

end;

( 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

( 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;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

suppose
ex F being Subset of Y st

( F is closed & not s in F & t in F ) ; :: thesis: contradiction

( 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;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