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 holds p is Point of
let Y be non empty SubSpace of X; :: thesis: for Z being non empty SubSpace of Y
for p being Point of holds p is Point of
let Z be non empty SubSpace of Y; :: thesis: for p being Point of holds p is Point of
let p be Point of ; :: thesis: p is Point of
p is Point of by PRE_TOPC:55;
hence p is Point of by PRE_TOPC:55; :: thesis: verum