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