theorem Th7: :: MFOLD_0:7

for M being non empty locally_euclidean with_boundary TopSpace
for p being Point of M
for n being Nat st ex U being a_neighborhood of p st M | U, Tdisk ((0. (TOP-REAL (n + 1))),1) are_homeomorphic holds
for pF being Point of (M | (Fr M)) st p = pF holds
ex U being a_neighborhood of pF st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic