let GX be non empty TopSpace; :: thesis: for x being Point of GX holds {x} is connected
let x be Point of GX; :: thesis: {x} is connected
assume not {x} is connected ; :: thesis: contradiction
then consider P, Q being Subset of GX such that
A1: {x} = P \/ Q and
A2: P,Q are_separated and
A3: P <> {} GX and
A4: Q <> {} GX by Th16;
P <> Q

proof

assume not P <> Q ; :: thesis: contradiction
then A5: P /\ Q = P ;
P misses Q by A2, Th2;
hence contradiction by A3, A5, XBOOLE_0:def 7; :: thesis: verum

end;

hence contradiction by A1, A3, A4, ZFMISC_1:44; :: thesis: verum