let GX be non empty TopSpace; :: thesis: for A being Subset of GX st A is_a_component_of GX holds
Component_of A = A
let A be Subset of GX; :: thesis: ( A is_a_component_of GX implies Component_of A = A )
assume A1: A is_a_component_of GX ; :: thesis: Component_of A = A
then A2: A is connected by CONNSP_1:def 5;
then A3: A c= Component_of A by Th1;
A <> {} GX by A1, CONNSP_1:34;
then Component_of A is connected by A2, Th5;
hence Component_of A = A by A1, A3, CONNSP_1:def 5; :: thesis: verum