let T, S1, S2 be non empty TopStruct ; :: thesis: ( S1,S2 are_homeomorphic & S1 is_Retract_of T implies S2 is_Retract_of T )
assume that
A1: S1,S2 are_homeomorphic and
A2: S1 is_Retract_of T ; :: thesis: S2 is_Retract_of T
consider G being Function of S1,S2 such that
A3: G is being_homeomorphism by A1;
consider H being Function of T,T such that
A4: H is continuous and
A5: H * H = H and
A6: Image H,S1 are_homeomorphic by A2;
take H ; :: according to WAYBEL18:def 8 :: thesis: ( H is continuous & H * H = H & Image H,S2 are_homeomorphic )
consider F being Function of (Image H),S1 such that
A7: F is being_homeomorphism by A6;
G * F is being_homeomorphism by A3, A7, TOPS_2:57;
hence ( H is continuous & H * H = H & Image H,S2 are_homeomorphic ) by A4, A5; :: thesis: verum