let p, q be Point of (1TopSp {x}); :: according to PRE_TOPC:def 10 :: thesis: ( p = q or ex b_{1}, b_{2} being Element of bool the carrier of (1TopSp {x}) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} ) )

assume A1: p <> q ; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of (1TopSp {x}) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )

p = x by TARSKI:def 1;

hence ex b_{1}, b_{2} being Element of bool the carrier of (1TopSp {x}) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )
by A1, TARSKI:def 1; :: thesis: verum

( b

assume A1: p <> q ; :: thesis: ex b

( b

p = x by TARSKI:def 1;

hence ex b

( b