set T = TopStruct(# 1,([#] (bool 1)) #);
A1: ( [#] the carrier of TopStruct(# 1,([#] (bool 1)) #) = the carrier of TopStruct(# 1,([#] (bool 1)) #) & ( 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 A1, 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 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 ` ) ) by CARD_1:87, TARSKI:def 1; :: thesis: verum