let GX be non empty TopSpace; :: thesis: for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds

Component_of A = Component_of B

let A, B be Subset of GX; :: thesis: ( A is connected & B is connected & A <> {} & A c= B implies Component_of A = Component_of B )

assume that

A1: A is connected and

A2: B is connected and

A3: A <> {} and

A4: A c= B ; :: thesis: Component_of A = Component_of B

B <> {} by A3, A4;

then A5: Component_of B is connected by A2, Th5;

A6: B c= Component_of B by A2, Th1;

then A7: A c= Component_of B by A4;

A8: Component_of B c= Component_of A

Component_of A c= Component_of B

Component_of A = Component_of B

let A, B be Subset of GX; :: thesis: ( A is connected & B is connected & A <> {} & A c= B implies Component_of A = Component_of B )

assume that

A1: A is connected and

A2: B is connected and

A3: A <> {} and

A4: A c= B ; :: thesis: Component_of A = Component_of B

B <> {} by A3, A4;

then A5: Component_of B is connected by A2, Th5;

A6: B c= Component_of B by A2, Th1;

then A7: A c= Component_of B by A4;

A8: Component_of B c= Component_of A

proof

A11:
Component_of A is connected
by A1, A3, Th5;
consider F being Subset-Family of GX such that

A9: for D being Subset of GX holds

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

A10: union F = Component_of A by Def1;

Component_of B in F by A7, A5, A9;

hence Component_of B c= Component_of A by A10, ZFMISC_1:74; :: thesis: verum

end;A9: for D being Subset of GX holds

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

A10: union F = Component_of A by Def1;

Component_of B in F by A7, A5, A9;

hence Component_of B c= Component_of A by A10, ZFMISC_1:74; :: thesis: verum

Component_of A c= Component_of B

proof

hence
Component_of A = Component_of B
by A8; :: thesis: verum
consider F being Subset-Family of GX such that

A12: for D being Subset of GX holds

( D in F iff ( D is connected & B c= D ) ) and

A13: union F = Component_of B by Def1;

B c= Component_of A by A6, A8;

then Component_of A in F by A11, A12;

hence Component_of A c= Component_of B by A13, ZFMISC_1:74; :: thesis: verum

end;A12: for D being Subset of GX holds

( D in F iff ( D is connected & B c= D ) ) and

A13: union F = Component_of B by Def1;

B c= Component_of A by A6, A8;

then Component_of A in F by A11, A12;

hence Component_of A c= Component_of B by A13, ZFMISC_1:74; :: thesis: verum