let GX be non empty TopSpace; :: thesis: for x, p being Point of GX st p in Component_of x holds
Component_of p = Component_of x
let x be Point of GX; :: thesis: for p being Point of GX st p in Component_of x holds
Component_of p = Component_of x
set A = Component_of x;
A1: Component_of x is a_component by Th40;
given p being Point of GX such that A2: p in Component_of x and
A3: Component_of p <> Component_of x ; :: thesis: contradiction
Component_of p is a_component by Th40;
then Component_of p misses Component_of x by A3, A1, Th1, Th34;
then A4: (Component_of p) /\ (Component_of x) = {} GX ;
p in Component_of p by Th38;
hence contradiction by A2, A4, XBOOLE_0:def 4; :: thesis: verum