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
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 & 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;
A11: Component_of A is connected by A1, A3, Th5;
Component_of A c= Component_of B
proof
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;
hence Component_of A = Component_of B by A8; :: thesis: verum