let GX be non empty TopSpace; :: thesis: for A being Subset of GX holds

( A is a_component 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 iff ex V being Subset of GX st

( V is connected & V <> {} & A = Component_of V ) )

( V is connected & V <> {} & A = Component_of V ) ) by A1; :: thesis: verum

( A is a_component 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 iff ex V being Subset of GX st

( V is connected & V <> {} & A = Component_of V ) )

A1: now :: thesis: ( A is a_component implies ex V being Subset of GX st

( V is connected & V <> {} & A = Component_of V ) )

( V is connected & V <> {} & A = Component_of V ) )

assume A2:
A is a_component
; :: thesis: ex V being Subset of GX st

( V is connected & V <> {} & A = Component_of V )

take V = A; :: thesis: ( V is connected & V <> {} & A = Component_of V )

thus ( V is connected & V <> {} & A = Component_of V ) by A2, Th7; :: thesis: verum

end;( V is connected & V <> {} & A = Component_of V )

take V = A; :: thesis: ( V is connected & V <> {} & A = Component_of V )

thus ( V is connected & V <> {} & A = Component_of V ) by A2, Th7; :: thesis: verum

now :: thesis: ( ex V being Subset of GX st

( V is connected & V <> {} & A = Component_of V ) implies A is a_component )

hence
( A is a_component iff ex V being Subset of GX st ( V is connected & V <> {} & A = Component_of V ) implies A is a_component )

given V being Subset of GX such that A3:
( V is connected & V <> {} & A = Component_of V )
; :: thesis: A is a_component

( A is connected & ( for B being Subset of GX st B is connected & A c= B holds

A = B ) ) by A3, Th5, Th6;

hence A is a_component by CONNSP_1:def 5; :: thesis: verum

end;( A is connected & ( for B being Subset of GX st B is connected & A c= B holds

A = B ) ) by A3, Th5, Th6;

hence A is a_component by CONNSP_1:def 5; :: thesis: verum

( V is connected & V <> {} & A = Component_of V ) ) by A1; :: thesis: verum