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

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