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

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