let GX be non empty TopSpace; :: thesis: for B being Subset of GX

for p being Point of GX st p in B holds

p in Component_of (p,B)

let B be Subset of GX; :: thesis: for p being Point of GX st p in B holds

p in Component_of (p,B)

let p be Point of GX; :: thesis: ( p in B implies p in Component_of (p,B) )

assume A1: p in B ; :: thesis: p in Component_of (p,B)

then reconsider B9 = B as non empty Subset of GX ;

reconsider q = p as Point of (GX | B9) by A1, PRE_TOPC:8;

q in Component_of q by CONNSP_1:38;

hence p in Component_of (p,B) by A1, Def7; :: thesis: verum

for p being Point of GX st p in B holds

p in Component_of (p,B)

let B be Subset of GX; :: thesis: for p being Point of GX st p in B holds

p in Component_of (p,B)

let p be Point of GX; :: thesis: ( p in B implies p in Component_of (p,B) )

assume A1: p in B ; :: thesis: p in Component_of (p,B)

then reconsider B9 = B as non empty Subset of GX ;

reconsider q = p as Point of (GX | B9) by A1, PRE_TOPC:8;

q in Component_of q by CONNSP_1:38;

hence p in Component_of (p,B) by A1, Def7; :: thesis: verum