let p, q be Point of (1TopSp {x}); :: according to PRE_TOPC:def 10 :: thesis: ( p = q or ex b₁, b₂ being Element of bool the carrier of (1TopSp {x}) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) )
assume A1: p <> q ; :: thesis: ex b₁, b₂ being Element of bool the carrier of (1TopSp {x}) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ )
p = x by TARSKI:def 1;
hence ex b₁, b₂ being Element of bool the carrier of (1TopSp {x}) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) by A1, TARSKI:def 1; :: thesis: verum