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 17 :: 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, Th18; :: thesis: verum