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 Z1:
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 16 :: thesis: ( 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 Z2:
p <> q
;
:: thesis: 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 W1:
(
G1 is
open &
G2 is
open )
and W2:
(
pp in G1 &
qq in G2 &
G1 misses G2 )
by Z1, Z2, PRE_TOPC:def 16;
reconsider H1 =
G1,
H2 =
G2 as
Subset of
TopStruct(# the
carrier of
T,the
topology of
T #) ;
take
H1
;
:: thesis: 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
;
:: thesis: ( H1 is open & H2 is open & p in H1 & q in H2 & H1 misses H2 )
thus
(
H1 is
open &
H2 is
open )
by W1, PRE_TOPC:60;
:: thesis: ( p in H1 & q in H2 & H1 misses H2 )
thus
(
p in H1 &
q in H2 &
H1 misses H2 )
by W2;
:: thesis: verum
end;
assume Z1:
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 16 :: thesis: ( 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 Z2:
p <> q
; :: thesis: 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
W1:
( G1 is open & G2 is open )
and
W2:
( pp in G1 & qq in G2 & G1 misses G2 )
by Z1, Z2, PRE_TOPC:def 16;
reconsider H1 = G1, H2 = G2 as Subset of T ;
take
H1
; :: thesis: 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
; :: thesis: ( H1 is open & H2 is open & p in H1 & q in H2 & H1 misses H2 )
thus
( H1 is open & H2 is open )
by W1, PRE_TOPC:60; :: thesis: ( p in H1 & q in H2 & H1 misses H2 )
thus
( p in H1 & q in H2 & H1 misses H2 )
by W2; :: thesis: verum