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 and
A2: S,Y are_homeomorphic by YELLOW16:59;
assume ( oContMaps X,Z is complete & oContMaps X,Z is continuous ) ; :: thesis: ( oContMaps X,Y is complete & oContMaps X,Y is continuous )
then A3: ( oContMaps X,S is complete & oContMaps X,S is continuous ) by A1, Th23;
oContMaps X,S, oContMaps X,Y are_isomorphic by A2, Th22;
hence ( oContMaps X,Y is complete & oContMaps X,Y is continuous ) by A3, WAYBEL15:11, WAYBEL20:18; :: thesis: verum