let T be TopStruct ; :: thesis: ( T is T_1 implies T is T_0 )
assume A1: T is T_1 ; :: thesis: T is T_0
let x be Point of T; :: according to PRE_TOPC:def 8 :: thesis: for y being Point of T st ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) holds
x = y
let y be Point of T; :: thesis: ( ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) implies x = y )
assume A2: for G being Subset of T st G is open holds
( x in G iff y in G ) ; :: thesis: x = y
assume x <> y ; :: thesis: contradiction
then consider G being Subset of T such that
A3: ( G is open & x in G ) and
A4: y in G ` by A1;
not y in G by A4, XBOOLE_0:def 5;
hence contradiction by A2, A3; :: thesis: verum