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 that
A1: A is connected and
A2: p in A ; :: thesis: Component_of p = Component_of A
( A c= Component_of A & Component_of A is a_component ) by A1, A2, Th1, Th8;
hence Component_of p = Component_of A by A2, CONNSP_1:41; :: thesis: verum