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

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