let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X holds incl X0 is continuous Function of X0,X
let X0 be non empty SubSpace of X; :: thesis: incl X0 is continuous Function of X0,X
id X is continuous Function of X,X by Th94;
hence incl X0 is continuous Function of X0,X by Th68; :: thesis: verum