let GX be non empty TopSpace; :: thesis: for A being Subset of GX
for p being Point of GX st A is connected & p in A holds
Component_of p = Component_of A
let A be Subset of GX; :: thesis: for p being Point of GX st A is connected & p in A holds
Component_of p = Component_of A
let p be Point of GX; :: thesis: ( A is connected & p in A implies Component_of p = Component_of A )
assume A1: ( A is connected & p in A ) ; :: thesis: Component_of p = Component_of A
then A2: A c= Component_of A by Th1;
Component_of A is_a_component_of GX by A1, Th8;
hence Component_of p = Component_of A by A1, A2, CONNSP_1:44; :: thesis: verum