let Z be monotone-convergence T_0-TopSpace; :: thesis: for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
Y is monotone-convergence
let Y be non empty SubSpace of Z; :: thesis: for f being continuous Function of Z,Y st f is being_a_retraction holds
Y is monotone-convergence
let f be continuous Function of Z,Y; :: thesis: ( f is being_a_retraction implies Y is monotone-convergence )
assume f is being_a_retraction ; :: thesis: Y is monotone-convergence
then Y is_a_retract_of Z ;
hence Y is monotone-convergence by WAYBEL25:36, YELLOW16:56; :: thesis: verum