let T be non empty TopSpace; :: thesis: for S being non empty SubSpace of T st S is_a_retract_of T holds
S is_Retract_of T
let S be non empty SubSpace of T; :: thesis: ( S is_a_retract_of T implies S is_Retract_of T )
reconsider g = incl S,T as continuous Function of S,T by Th56;
given f being continuous Function of T,S such that A1: f is being_a_retraction ; :: according to BORSUK_1:def 20 :: thesis: S is_Retract_of T
take g ; :: according to WAYBEL25:def 1 :: thesis: ex b₁ being Element of bool [:the carrier of T,the carrier of S:] st b₁ * g = id S
take f ; :: thesis: f * g = id S
thus f * g = id S by A1, Th57; :: thesis: verum