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