let GX be non empty TopSpace; :: thesis: for A being Subset of GX
for x being Point of GX st A = Component_of x holds
for p being Point of GX st p in A holds
Component_of p = A
let A be Subset of GX; :: thesis: for x being Point of GX st A = Component_of x holds
for p being Point of GX st p in A holds
Component_of p = A
let x be Point of GX; :: thesis: ( A = Component_of x implies for p being Point of GX st p in A holds
Component_of p = A )
assume A1: A = Component_of x ; :: thesis: for p being Point of GX st p in A holds
Component_of p = A
given p being Point of GX such that A2: p in A and
A3: Component_of p <> A ; :: thesis: contradiction
( Component_of p is_a_component_of GX & A is_a_component_of GX ) by A1, Th43;
then Component_of p misses A by A3, Th2, Th36;
then A4: (Component_of p) /\ A = {} GX by XBOOLE_0:def 7;
p in Component_of p by Th40;
hence contradiction by A2, A4, XBOOLE_0:def 4; :: thesis: verum