let GX be non empty TopSpace; :: thesis: for A being Subset of GX

for x being Point of GX st A is a_component & x in A holds

A = Component_of x

let A be Subset of GX; :: thesis: for x being Point of GX st A is a_component & x in A holds

A = Component_of x

let x be Point of GX; :: thesis: ( A is a_component & x in A implies A = Component_of x )

assume that

A1: A is a_component and

A2: x in A ; :: thesis: A = Component_of x

x in Component_of x by Th38;

then A /\ (Component_of x) <> {} by A2, XBOOLE_0:def 4;

then A3: A meets Component_of x ;

A4: Component_of x is a_component by Th40;

assume A <> Component_of x ; :: thesis: contradiction

hence contradiction by A1, A3, A4, Th1, Th34; :: thesis: verum

for x being Point of GX st A is a_component & x in A holds

A = Component_of x

let A be Subset of GX; :: thesis: for x being Point of GX st A is a_component & x in A holds

A = Component_of x

let x be Point of GX; :: thesis: ( A is a_component & x in A implies A = Component_of x )

assume that

A1: A is a_component and

A2: x in A ; :: thesis: A = Component_of x

x in Component_of x by Th38;

then A /\ (Component_of x) <> {} by A2, XBOOLE_0:def 4;

then A3: A meets Component_of x ;

A4: Component_of x is a_component by Th40;

assume A <> Component_of x ; :: thesis: contradiction

hence contradiction by A1, A3, A4, Th1, Th34; :: thesis: verum