set T = TopStruct(# 1,([#] (bool 1)) #);
A: [#] the carrier of TopStruct(# 1,([#] (bool 1)) #) = the carrier of TopStruct(# 1,([#] (bool 1)) #) ;
B: for a being Subset-Family of TopStruct(# 1,([#] (bool 1)) #) st a c= the topology of TopStruct(# 1,([#] (bool 1)) #) holds
union a in the topology of TopStruct(# 1,([#] (bool 1)) #) ;
for a, b being Subset of TopStruct(# 1,([#] (bool 1)) #) st a in the topology of TopStruct(# 1,([#] (bool 1)) #) & b in the topology of TopStruct(# 1,([#] (bool 1)) #) holds
a /\ b in the topology of TopStruct(# 1,([#] (bool 1)) #) ;
then reconsider T = TopStruct(# 1,([#] (bool 1)) #) as non empty TopSpace by A, B, Def1;
take T ; :: 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 ` ) )
( p = 0 & q = 0 ) by CARD_1:87, TARSKI:def 1;
hence ( p <> q implies ex G being Subset of T st
( G is open & p in G & q in G ` ) ) ; :: thesis: verum