let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X
for x being Point of X st x in the carrier of X0 holds
(incl X0) . x = x
let X0 be non empty SubSpace of X; :: thesis: for x being Point of X st x in the carrier of X0 holds
(incl X0) . x = x
let x be Point of X; :: thesis: ( x in the carrier of X0 implies (incl X0) . x = x )
assume x in the carrier of X0 ; :: thesis: (incl X0) . x = x
hence (incl X0) . x = (id X) . x by FUNCT_1:49
.= x ;
:: thesis: verum