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