let T be non empty TopSpace; :: thesis: for S being non empty SubSpace of T holds incl (S,T) is continuous
let S be non empty SubSpace of T; :: thesis: incl (S,T) is continuous
incl (S,T) = id S by BORSUK_1:35, YELLOW_9:def 1;
hence incl (S,T) is continuous by PRE_TOPC:56; :: thesis: verum