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

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