:: deftheorem defines is_Retract_of WAYBEL18:def 8 :
for X, Y being TopStruct holds
( X is_Retract_of Y iff ex f being Function of Y,Y st
( f is continuous & f * f = f & Image f,X are_homeomorphic ) );