for n being Nat
for A being non empty convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds
for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds
not FR is_a_retract_of (TOP-REAL n) | A