let X be non trivial anti-discrete TopStruct ; :: thesis: not X is T_0

now :: thesis: ex x, y being Point of X st

( x <> y & ( for V being Subset of X holds

( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds

( not W is open or x in W or not y in W ) ) )

hence
not X is T_0
; :: thesis: verum( x <> y & ( for V being Subset of X holds

( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds

( not W is open or x in W or not y in W ) ) )

consider x, y being Point of X such that

A1: x <> y by STRUCT_0:def 10;

take x = x; :: thesis: ex y being Point of X st

( x <> y & ( for V being Subset of X holds

( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds

( not W is open or x in W or not y in W ) ) )

take y = y; :: thesis: ( x <> y & ( for V being Subset of X holds

( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds

( not W is open or x in W or not y in W ) ) )

thus x <> y by A1; :: thesis: ( ( for V being Subset of X holds

( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds

( not W is open or x in W or not y in W ) ) )

( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds

( not W is open or x in W or not y in W ) ) ) by A2; :: thesis: verum

end;A1: x <> y by STRUCT_0:def 10;

take x = x; :: thesis: ex y being Point of X st

( x <> y & ( for V being Subset of X holds

( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds

( not W is open or x in W or not y in W ) ) )

take y = y; :: thesis: ( x <> y & ( for V being Subset of X holds

( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds

( not W is open or x in W or not y in W ) ) )

thus x <> y by A1; :: thesis: ( ( for V being Subset of X holds

( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds

( not W is open or x in W or not y in W ) ) )

A2: now :: thesis: for V being Subset of X st V is open & y in V holds

x in V

x in V

let V be Subset of X; :: thesis: ( V is open & y in V implies x in V )

assume V is open ; :: thesis: ( y in V implies x in V )

then A3: ( V = {} or V = the carrier of X ) by TDLAT_3:18;

assume y in V ; :: thesis: x in V

hence x in V by A3; :: thesis: verum

end;assume V is open ; :: thesis: ( y in V implies x in V )

then A3: ( V = {} or V = the carrier of X ) by TDLAT_3:18;

assume y in V ; :: thesis: x in V

hence x in V by A3; :: thesis: verum

now :: thesis: for V being Subset of X st V is open & x in V holds

y in V

hence
( ( for V being Subset of X holds y in V

let V be Subset of X; :: thesis: ( V is open & x in V implies y in V )

assume V is open ; :: thesis: ( x in V implies y in V )

then A4: ( V = {} or V = the carrier of X ) by TDLAT_3:18;

assume x in V ; :: thesis: y in V

hence y in V by A4; :: thesis: verum

end;assume V is open ; :: thesis: ( x in V implies y in V )

then A4: ( V = {} or V = the carrier of X ) by TDLAT_3:18;

assume x in V ; :: thesis: y in V

hence y in V by A4; :: thesis: verum

( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds

( not W is open or x in W or not y in W ) ) ) by A2; :: thesis: verum