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 Th53;
given f being continuous Function of T,S such that A1: f is being_a_retraction ; :: according to BORSUK_1:def 17 :: 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, Th54; :: thesis: verum