let T be TopStruct ; :: thesis: ( T is T_2 implies T is T_1 )
assume Z1: T is T_2 ; :: thesis: T is T_1
let p, q be Point of T; :: according to PRE_TOPC:def 15 :: thesis: ( p <> q implies ex G being Subset of T st
( G is open & p in G & q in G ` ) )
assume p <> q ; :: thesis: ex G being Subset of T st
( G is open & p in G & q in G ` )
then consider G1, G2 being Subset of T such that
W1: ( G1 is open & G2 is open ) and
W2: ( p in G1 & q in G2 ) and
W3: G1 misses G2 by Z1, Def16;
take G1 ; :: thesis: ( G1 is open & p in G1 & q in G1 ` )
thus G1 is open by W1; :: thesis: ( p in G1 & q in G1 ` )
thus p in G1 by W2; :: thesis: q in G1 `
G2 c= G1 ` by W3, SUBSET_1:43;
hence q in G1 ` by W2; :: thesis: verum