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 A1: ( A is connected & B is connected & A <> {} & A c= B ) ; :: thesis: Component_of A = Component_of B
then A2: B <> {} ;
A3: B c= Component_of B by A1, Th1;
then A4: A c= Component_of B by A1, XBOOLE_1:1;
A5: Component_of B is connected by A1, A2, Th5;
A6: Component_of A is connected by A1, Th5;
A7: Component_of B c= Component_of A

proof

consider F being Subset-Family of GX such that
A8: ( ( for D being Subset of GX holds
( D in F iff ( D is connected & A c= D ) ) ) & union F = Component_of A ) by Def1;
Component_of B in F by A4, A5, A8;
hence Component_of B c= Component_of A by A8, ZFMISC_1:92; :: thesis: verum

end;

Component_of A c= Component_of B

proof

consider F being Subset-Family of GX such that
A9: ( ( for D being Subset of GX holds
( D in F iff ( D is connected & B c= D ) ) ) & union F = Component_of B ) by Def1;
B c= Component_of A by A3, A7, XBOOLE_1:1;
then Component_of A in F by A6, A9;
hence Component_of A c= Component_of B by A9, ZFMISC_1:92; :: thesis: verum

end;

hence Component_of A = Component_of B by A7, XBOOLE_0:def 10; :: thesis: verum