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 holds
oContMaps X,Y is_a_retract_of oContMaps X,Z
let Z be monotone-convergence T_0-TopSpace; :: thesis: for Y being non empty SubSpace of Z st Y is_a_retract_of Z holds
oContMaps X,Y is_a_retract_of oContMaps X,Z
let Y be non empty SubSpace of Z; :: thesis: ( Y is_a_retract_of Z implies oContMaps X,Y is_a_retract_of oContMaps X,Z )
given f being continuous Function of Z,Y such that A1: f is being_a_retraction ; :: according to BORSUK_1:def 20 :: thesis: oContMaps X,Y is_a_retract_of oContMaps X,Z
take oContMaps X,f ; :: according to YELLOW16:def 3 :: thesis: oContMaps X,f is_a_retraction_of oContMaps X,Z, oContMaps X,Y
thus oContMaps X,f is_a_retraction_of oContMaps X,Z, oContMaps X,Y by A1, Th19; :: thesis: verum