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
; T is T_1
let p, q be Point of T; PRE_TOPC:def 9 ( 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; verum