let X be non empty TopSpace; :: thesis: for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z st Y is_a_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 Z be monotone-convergence T_0-TopSpace; :: thesis: for Y being non empty SubSpace of Z st Y is_a_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 be non empty SubSpace of Z; :: thesis: ( Y is_a_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_a_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 A1: oContMaps X,Y is_a_retract_of oContMaps X,Z by Th20;
assume ( oContMaps X,Z is complete & oContMaps X,Z is continuous ) ; :: thesis: ( oContMaps X,Y is complete & oContMaps X,Y is continuous )
hence ( oContMaps X,Y is complete & oContMaps X,Y is continuous ) by A1, YELLOW16:23, YELLOW16:24; :: thesis: verum