let GX be TopSpace; :: thesis: for V being Subset of GX st ex A being Subset of GX st

( A is connected & V c= A ) holds

V c= Component_of V

let V be Subset of GX; :: thesis: ( ex A being Subset of GX st

( A is connected & V c= A ) implies V c= Component_of V )

given A being Subset of GX such that A1: ( A is connected & V c= A ) ; :: thesis: V c= Component_of V

consider F being Subset-Family of GX such that

A2: for A being Subset of GX holds

( A in F iff ( A is connected & V c= A ) ) and

A3: Component_of V = union F by Def1;

A4: for A being set st A in F holds

V c= A by A2;

F <> {} by A1, A2;

then A5: V c= meet F by A4, SETFAM_1:5;

meet F c= union F by SETFAM_1:2;

hence V c= Component_of V by A3, A5; :: thesis: verum

( A is connected & V c= A ) holds

V c= Component_of V

let V be Subset of GX; :: thesis: ( ex A being Subset of GX st

( A is connected & V c= A ) implies V c= Component_of V )

given A being Subset of GX such that A1: ( A is connected & V c= A ) ; :: thesis: V c= Component_of V

consider F being Subset-Family of GX such that

A2: for A being Subset of GX holds

( A in F iff ( A is connected & V c= A ) ) and

A3: Component_of V = union F by Def1;

A4: for A being set st A in F holds

V c= A by A2;

F <> {} by A1, A2;

then A5: V c= meet F by A4, SETFAM_1:5;

meet F c= union F by SETFAM_1:2;

hence V c= Component_of V by A3, A5; :: thesis: verum