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