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

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