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

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