let GX be non empty TopSpace; :: thesis: for V, C being Subset of GX st V is connected & C is connected & Component_of V c= C holds

C = Component_of V

let V, C be Subset of GX; :: thesis: ( V is connected & C is connected & Component_of V c= C implies C = Component_of V )

assume that

A1: V is connected and

A2: C is connected ; :: thesis: ( not Component_of V c= C or C = Component_of V )

assume A3: Component_of V c= C ; :: thesis: C = Component_of V

consider F being Subset-Family of GX such that

A4: for A being Subset of GX holds

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

A5: Component_of V = union F by Def1;

V c= Component_of V by A1, Th1;

then V c= C by A3;

then C in F by A2, A4;

then C c= Component_of V by A5, ZFMISC_1:74;

hence C = Component_of V by A3; :: thesis: verum

C = Component_of V

let V, C be Subset of GX; :: thesis: ( V is connected & C is connected & Component_of V c= C implies C = Component_of V )

assume that

A1: V is connected and

A2: C is connected ; :: thesis: ( not Component_of V c= C or C = Component_of V )

assume A3: Component_of V c= C ; :: thesis: C = Component_of V

consider F being Subset-Family of GX such that

A4: for A being Subset of GX holds

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

A5: Component_of V = union F by Def1;

V c= Component_of V by A1, Th1;

then V c= C by A3;

then C in F by A2, A4;

then C c= Component_of V by A5, ZFMISC_1:74;

hence C = Component_of V by A3; :: thesis: verum