let T be TopStruct ; :: thesis: ( T is T_1 implies T is T_0 )
assume Z1: T is T_1 ; :: thesis: T is T_0
let x be Point of T; :: according to PRE_TOPC:def 14 :: 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 Z2: 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
W1: G is open and
W2: ( x in G & y in G ` ) by Z1, Def15;
not y in G by W2, XBOOLE_0:def 5;
hence contradiction by W1, W2, Z2; :: thesis: verum