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 Def9;
hence for p being Point of A holds p is Point of T by TARSKI:def 3; :: thesis: verum