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