for T being non empty TopSpace
for S being non empty SubSpace of T
for f being continuous Function of T,S st f is being_a_retraction holds
f * (incl (S,T)) = id S