let GX be non empty TopSpace; :: thesis: for B being Subset of GX
for p being Point of GX st p in B holds
Component_of (p,B) is connected
let B be Subset of GX; :: thesis: for p being Point of GX st p in B holds
Component_of (p,B) is connected
let p be Point of GX; :: thesis: ( p in B implies Component_of (p,B) is connected )
assume A1: p in B ; :: thesis: Component_of (p,B) is connected
then reconsider B9 = B as non empty Subset of GX ;
( Component_of (Down (p,B9)) is connected & Component_of (p,B) = Component_of (Down (p,B)) ) by A1, Th27;
hence Component_of (p,B) is connected by CONNSP_1:23; :: thesis: verum