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) = Component_of (Down (p,B))

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

Component_of (p,B) = Component_of (Down (p,B))

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

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

then p = Down (p,B) by Def3;

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

for p being Point of GX st p in B holds

Component_of (p,B) = Component_of (Down (p,B))

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

Component_of (p,B) = Component_of (Down (p,B))

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

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

then p = Down (p,B) by Def3;

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