let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X holds modid X,X0 = id X
let X0 be non empty SubSpace of X; :: thesis: modid X,X0 = id X
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
modid X,A = modid X,X0 by Def11;
hence modid X,X0 = id X ; :: thesis: verum