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