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