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

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