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:1, YELLOW_9:def 1;
hence incl (S,T) is continuous by PRE_TOPC:26; :: thesis: verum