now :: thesis: {x} is connected

hence
for bassume
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 Th15;

P <> Q

end;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 Th15;

P <> Q

proof

hence
contradiction
by A1, A3, A4, ZFMISC_1:38; :: thesis: verum
assume
not P <> Q
; :: thesis: contradiction

then A5: P /\ Q = P ;

P misses Q by A2, Th1;

hence contradiction by A3, A5; :: thesis: verum

end;then A5: P /\ Q = P ;

P misses Q by A2, Th1;

hence contradiction by A3, A5; :: thesis: verum

b