let T be non empty TopStruct ; :: thesis: for A being non empty SubSpace of T
for p being Point of A holds p is Point of T
let A be non empty SubSpace of T; :: thesis: for p being Point of A holds p is Point of T
[#] A c= [#] T by Def4;
hence for p being Point of A holds p is Point of T ; :: thesis: verum