let M be non empty MetrSpace; :: thesis: for A being non empty SubSpace of M
for p being Point of holds p is Point of
let A be non empty SubSpace of M; :: thesis: for p being Point of holds p is Point of
let p be Point of ; :: thesis: p is Point of
( p in the carrier of A & the carrier of A c= the carrier of M ) by Def1;
hence p is Point of ; :: thesis: verum