let X be non empty TopSpace; :: thesis: for Y, Z being monotone-convergence T_0-TopSpace st Y is_Retract_of Z & oContMaps X,Z is complete & oContMaps X,Z is continuous holds
( oContMaps X,Y is complete & oContMaps X,Y is continuous )
let Y, Z be monotone-convergence T_0-TopSpace; :: thesis: ( Y is_Retract_of Z & oContMaps X,Z is complete & oContMaps X,Z is continuous implies ( oContMaps X,Y is complete & oContMaps X,Y is continuous ) )
assume Y is_Retract_of Z ; :: thesis: ( not oContMaps X,Z is complete or not oContMaps X,Z is continuous or ( oContMaps X,Y is complete & oContMaps X,Y is continuous ) )
then consider S being non empty SubSpace of Z such that
A1: ( S is_a_retract_of Z & S,Y are_homeomorphic ) by YELLOW16:59;
A2: oContMaps X,S, oContMaps X,Y are_isomorphic by A1, Th22;
assume ( oContMaps X,Z is complete & oContMaps X,Z is continuous ) ; :: thesis: ( oContMaps X,Y is complete & oContMaps X,Y is continuous )
then ( oContMaps X,S is complete & oContMaps X,S is continuous ) by A1, Th23;
hence ( oContMaps X,Y is complete & oContMaps X,Y is continuous ) by A2, WAYBEL15:11, WAYBEL20:18; :: thesis: verum