set T = TopStruct(# {{}},([#] (bool {{}})) #);
A1: ( [#] the carrier of TopStruct(# {{}},([#] (bool {{}})) #) = the carrier of TopStruct(# {{}},([#] (bool {{}})) #) & ( for a being Subset-Family of TopStruct(# {{}},([#] (bool {{}})) #) st a c= the topology of TopStruct(# {{}},([#] (bool {{}})) #) holds
union a in the topology of TopStruct(# {{}},([#] (bool {{}})) #) ) ) ;
for a, b being Subset of TopStruct(# {{}},([#] (bool {{}})) #) st a in the topology of TopStruct(# {{}},([#] (bool {{}})) #) & b in the topology of TopStruct(# {{}},([#] (bool {{}})) #) holds
a /\ b in the topology of TopStruct(# {{}},([#] (bool {{}})) #) ;
then reconsider T = TopStruct(# {{}},([#] (bool {{}})) #) 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 9 :: thesis: ( p <> q implies ex G being Subset of T st
( G is open & p in G & q in G ` ) )
p = {} by TARSKI:def 1;
hence ( p <> q implies ex G being Subset of T st
( G is open & p in G & q in G ` ) ) by TARSKI:def 1; :: thesis: verum