let T be TopStruct ; :: thesis: ( T is T_2 implies T is T_1 )
assume A5: T is T_2 ; :: thesis: T is T_1
let p, q be Point of T; :: according to PRE_TOPC:def 9 :: 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
A6: G1 is open and
G2 is open and
A7: p in G1 and
A8: q in G2 and
A9: G1 misses G2 by A5;
take G1 ; :: thesis: ( G1 is open & p in G1 & q in G1 ` )
thus G1 is open by A6; :: thesis: ( p in G1 & q in G1 ` )
thus p in G1 by A7; :: thesis: q in G1 `
G2 c= G1 ` by A9, SUBSET_1:23;
hence q in G1 ` by A8; :: thesis: verum