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