let GX be non empty TopSpace; :: thesis: for A being Subset of GX holds
( A is_a_component_of GX iff ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V ) )
let A be Subset of GX; :: thesis: ( A is_a_component_of GX iff ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V ) )

A1: now

assume A2: A is_a_component_of GX ; :: thesis: ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V )
then A3: ( A <> {} GX & A is connected ) by CONNSP_1:34, CONNSP_1:def 5;
take V = A; :: thesis: ( V is connected & V <> {} & A = Component_of V )
thus ( V is connected & V <> {} & A = Component_of V ) by A2, A3, Th7; :: thesis: verum

end;

now

given V being Subset of GX such that A4: V is connected and
A5: V <> {} and
A6: A = Component_of V ; :: thesis: A is_a_component_of GX
A7: A is connected by A4, A5, A6, Th5;
for B being Subset of GX st B is connected & A c= B holds
A = B by A4, A6, Th6;
hence A is_a_component_of GX by A7, CONNSP_1:def 5; :: thesis: verum

end;

hence ( A is_a_component_of GX iff ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V ) ) by A1; :: thesis: verum