let T be TopSpace; ( 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 )
( TopStruct(# the carrier of T, the topology of T #) is T_2 implies T is T_2 )proof
assume A1:
T is
T_2
;
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 #);
PRE_TOPC:def 10 ( p = q or ex b1, b2 being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A2:
p <> q
;
ex b1, b2 being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
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
;
ex b1 being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) st
( H1 is open & b1 is open & p in H1 & q in b1 & H1 misses b1 )
take
H2
;
( 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;
( p in H1 & q in H2 & H1 misses H2 )
thus
(
p in H1 &
q in H2 &
H1 misses H2 )
by A5, A6, A7;
verum
end;
assume A8:
TopStruct(# the carrier of T, the topology of T #) is T_2
; T is T_2
let p, q be Point of T; PRE_TOPC:def 10 ( p = q or ex b1, b2 being Element of K10( the carrier of T) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A9:
p <> q
; ex b1, b2 being Element of K10( the carrier of T) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
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
; ex b1 being Element of K10( the carrier of T) st
( H1 is open & b1 is open & p in H1 & q in b1 & H1 misses b1 )
take
H2
; ( 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; ( p in H1 & q in H2 & H1 misses H2 )
thus
( p in H1 & q in H2 & H1 misses H2 )
by A12, A13, A14; verum