let GX be non empty TopSpace; :: thesis: for B being Subset of
for p being Point of st p in B holds
Component_of p,B = Component_of (Down p,B)
let B be Subset of ; :: thesis: for p being Point of st p in B holds
Component_of p,B = Component_of (Down p,B)
let p be Point of ; :: 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