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
B c= Component_of A
let A, B be Subset of GX; :: thesis: ( A is connected & B is connected & A <> {} & A c= B implies B c= Component_of A )
assume A1: ( A is connected & B is connected & A <> {} & A c= B ) ; :: thesis: B c= Component_of A
then Component_of A = Component_of B by Th12;
hence B c= Component_of A by A1, Th1; :: thesis: verum