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