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

( A is a_component iff ex x being Point of GX st A = Component_of x )

let A be Subset of GX; :: thesis: ( A is a_component iff ex x being Point of GX st A = Component_of x )

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

A = B by A5, Th39;

hence A is a_component by A5; :: thesis: verum

( A is a_component iff ex x being Point of GX st A = Component_of x )

let A be Subset of GX; :: thesis: ( A is a_component iff ex x being Point of GX st A = Component_of x )

hereby :: thesis: ( ex x being Point of GX st A = Component_of x implies A is a_component )

given x being Point of GX such that A5:
A = Component_of x
; :: thesis: A is a_component assume A1:
A is a_component
; :: thesis: ex x being Point of GX st A = Component_of x

then A <> {} GX ;

then consider y being Point of GX such that

A2: y in A by PRE_TOPC:12;

take x = y; :: thesis: A = Component_of x

consider F being Subset-Family of GX such that

A3: for B being Subset of GX holds

( B in F iff ( B is connected & x in B ) ) and

A4: union F = Component_of x by Def7;

A in F by A1, A2, A3;

then A c= union F by ZFMISC_1:74;

hence A = Component_of x by A1, A4; :: thesis: verum

end;then A <> {} GX ;

then consider y being Point of GX such that

A2: y in A by PRE_TOPC:12;

take x = y; :: thesis: A = Component_of x

consider F being Subset-Family of GX such that

A3: for B being Subset of GX holds

( B in F iff ( B is connected & x in B ) ) and

A4: union F = Component_of x by Def7;

A in F by A1, A2, A3;

then A c= union F by ZFMISC_1:74;

hence A = Component_of x by A1, A4; :: thesis: verum

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

A = B by A5, Th39;

hence A is a_component by A5; :: thesis: verum