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 ) ) )
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 ) ) )
A2: now :: thesis: for V being Subset of X st V is open & y in V holds
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;
now :: thesis: for V being Subset of X st V is open & x in V 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;
hence ( ( 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 ) ) ) by A2; :: thesis: verum
end;
hence not X is T_0 ; :: thesis: verum