let Y be non empty TopSpace; :: thesis: for W being non empty SubSpace of Y holds corestr (incl W) is being_homeomorphism
let W be non empty SubSpace of Y; :: thesis: corestr (incl W) is being_homeomorphism
set ci = corestr (incl W);
thus dom (corestr (incl W)) = [#] W by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng (corestr (incl W)) = [#] (Image (incl W)) & corestr (incl W) is one-to-one & corestr (incl W) is continuous & (corestr (incl W)) /" is continuous )
thus A1: rng (corestr (incl W)) = [#] (Image (incl W)) by FUNCT_2:def 3; :: thesis: ( corestr (incl W) is one-to-one & corestr (incl W) is continuous & (corestr (incl W)) /" is continuous )
A2: corestr (incl W) = incl W by WAYBEL18:def 7
.= (id Y) | W by TMAP_1:def 6
.= (id the carrier of Y) | the carrier of W by TMAP_1:def 4 ;
hence A3: corestr (incl W) is one-to-one by FUNCT_1:52; :: thesis: ( corestr (incl W) is continuous & (corestr (incl W)) /" is continuous )
A4: for P being Subset of W st P is open holds
((corestr (incl W)) /") " P is open

proof

let P be Subset of W; :: thesis: ( P is open implies ((corestr (incl W)) /") " P is open )
assume P in the topology of W ; :: according to PRE_TOPC:def 2 :: thesis: ((corestr (incl W)) /") " P is open
then A5: ex Q being Subset of Y st
( Q in the topology of Y & P = Q /\ ([#] W) ) by PRE_TOPC:def 4;
A6: the carrier of W is non empty Subset of Y by BORSUK_1:1;
then A7: P is Subset of Y by XBOOLE_1:1;
A8: [#] W = rng ((id the carrier of Y) | the carrier of W) by A6, Th2
.= rng ((id Y) | W) by TMAP_1:def 4
.= rng (incl W) by TMAP_1:def 6
.= [#] (Image (incl W)) by WAYBEL18:9 ;
((corestr (incl W)) /") " P = ((id the carrier of Y) | the carrier of W) .: P by A1, A2, A3, TOPS_2:54
.= (id the carrier of Y) .: P by FUNCT_2:97
.= P by A7, FUNCT_1:92 ;
hence ((corestr (incl W)) /") " P in the topology of (Image (incl W)) by A5, A8, PRE_TOPC:def 4; :: according to PRE_TOPC:def 2 :: thesis: verum

end;

thus corestr (incl W) is continuous by WAYBEL18:10; :: thesis: (corestr (incl W)) /" is continuous
[#] W <> {} ;
hence (corestr (incl W)) /" is continuous by A4, TOPS_2:43; :: thesis: verum