let X be non empty TopSpace; :: thesis: for Y being non empty SubSpace of X
for Z being non empty SubSpace of Y
for p being Point of Z holds p is Point of X
let Y be non empty SubSpace of X; :: thesis: for Z being non empty SubSpace of Y
for p being Point of Z holds p is Point of X
let Z be non empty SubSpace of Y; :: thesis: for p being Point of Z holds p is Point of X
let p be Point of Z; :: thesis: p is Point of X
p is Point of Y by PRE_TOPC:25;
hence p is Point of X by PRE_TOPC:25; :: thesis: verum