let GX be non empty TopSpace; :: thesis: for B being Subset of
for p being Point of st p in B holds
Component_of p,B is connected
let B be Subset of ; :: thesis: for p being Point of st p in B holds
Component_of p,B is connected
let p be Point of ; :: 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 B' = B as non empty Subset of ;
( Component_of (Down p,B') is connected & Component_of p,B = Component_of (Down p,B) ) by A1, Th27, CONNSP_1:41;
hence Component_of p,B is connected by CONNSP_1:24; :: thesis: verum