let T be TopSpace; :: thesis: ( T is T_2 iff TopStruct(# the carrier of T, the topology of T #) is T_2 )
thus ( T is T_2 implies TopStruct(# the carrier of T, the topology of T #) is T_2 ) :: thesis: ( TopStruct(# the carrier of T, the topology of T #) is T_2 implies T is T_2 )

proof

assume A1: T is T_2 ; :: thesis: TopStruct(# the carrier of T, the topology of T #) is T_2
let p, q be Point of TopStruct(# the carrier of T, the topology of T #); :: according to PRE_TOPC:def 10 :: thesis: ( p = q or ex b₁, b₂ being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) )
assume A2: p <> q ; :: thesis: ex b₁, b₂ being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ )
reconsider pp = p, qq = q as Point of T ;
consider G1, G2 being Subset of T such that
A3: G1 is open and
A4: G2 is open and
A5: pp in G1 and
A6: qq in G2 and
A7: G1 misses G2 by A1, A2;
reconsider H1 = G1, H2 = G2 as Subset of TopStruct(# the carrier of T, the topology of T #) ;
take H1 ; :: thesis: ex b₁ being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) st
( H1 is open & b₁ is open & p in H1 & q in b₁ & H1 misses b₁ )
take H2 ; :: thesis: ( H1 is open & H2 is open & p in H1 & q in H2 & H1 misses H2 )
thus ( H1 is open & H2 is open ) by A3, A4; :: thesis: ( p in H1 & q in H2 & H1 misses H2 )
thus ( p in H1 & q in H2 & H1 misses H2 ) by A5, A6, A7; :: thesis: verum

end;

assume A8: TopStruct(# the carrier of T, the topology of T #) is T_2 ; :: thesis: T is T_2
let p, q be Point of T; :: according to PRE_TOPC:def 10 :: thesis: ( p = q or ex b₁, b₂ being Element of K10( the carrier of T) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) )
assume A9: p <> q ; :: thesis: ex b₁, b₂ being Element of K10( the carrier of T) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ )
reconsider pp = p, qq = q as Point of TopStruct(# the carrier of T, the topology of T #) ;
consider G1, G2 being Subset of TopStruct(# the carrier of T, the topology of T #) such that
A10: G1 is open and
A11: G2 is open and
A12: pp in G1 and
A13: qq in G2 and
A14: G1 misses G2 by A8, A9;
reconsider H1 = G1, H2 = G2 as Subset of T ;
take H1 ; :: thesis: ex b₁ being Element of K10( the carrier of T) st
( H1 is open & b₁ is open & p in H1 & q in b₁ & H1 misses b₁ )
take H2 ; :: thesis: ( H1 is open & H2 is open & p in H1 & q in H2 & H1 misses H2 )
thus ( H1 is open & H2 is open ) by A10, A11; :: thesis: ( p in H1 & q in H2 & H1 misses H2 )
thus ( p in H1 & q in H2 & H1 misses H2 ) by A12, A13, A14; :: thesis: verum