let R, T be non empty TopSpace; :: thesis: ( R is_Retract_of T iff ex S being non empty SubSpace of T st
( S is_a_retract_of T & S,R are_homeomorphic ) )

hereby :: thesis: ( ex S being non empty SubSpace of T st
( S is_a_retract_of T & S,R are_homeomorphic ) implies R is_Retract_of T )

assume R is_Retract_of T ; :: thesis: ex S being non empty SubSpace of T st
( S is_a_retract_of T & S,R are_homeomorphic )
then consider f being Function of T,T such that
A1: ( f is continuous & f * f = f & Image f,R are_homeomorphic ) by WAYBEL18:def 8;
reconsider S = Image f as non empty SubSpace of T ;
take S = S; :: thesis: ( S is_a_retract_of T & S,R are_homeomorphic )
f = corestr f by WAYBEL18:def 7;
then reconsider f = f as continuous Function of T,S by A1, WAYBEL18:11;
( [#] S = the carrier of S & [#] T = the carrier of T ) ;
then the carrier of S c= the carrier of T by PRE_TOPC:def 9;
then reconsider rf = rng f as Subset of T by XBOOLE_1:1;

now

let x be Point of T; :: thesis: ( x in the carrier of S implies f . x = x )
assume x in the carrier of S ; :: thesis: f . x = x
then x in [#] (T | rf) by WAYBEL18:def 6;
then x in rng f by PRE_TOPC:def 10;
then ex y being set st
( y in dom f & x = f . y ) by FUNCT_1:def 5;
hence f . x = x by A1, FUNCT_1:23; :: thesis: verum

end;

then f is being_a_retraction by BORSUK_1:def 19;
hence ( S is_a_retract_of T & S,R are_homeomorphic ) by A1, BORSUK_1:def 20; :: thesis: verum

end;

given S being non empty SubSpace of T such that A2: ( S is_a_retract_of T & S,R are_homeomorphic ) ; :: thesis: R is_Retract_of T
thus R is_Retract_of T by A2, Th55, Th58; :: thesis: verum