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:24; :: thesis: verum