let n be Nat; :: thesis: 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
set T = TOP-REAL n;
A1: n in NAT by ORDINAL1:def 12;
set cB = cl_Ball ((0. (TOP-REAL n)),1);
set S = Sphere ((0. (TOP-REAL n)),1);
A2: [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;
then reconsider s = Sphere ((0. (TOP-REAL n)),1) as Subset of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A1, TOPREAL9:17;
A3: (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)) = ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) | s by A1, PRE_TOPC:7, TOPREAL9:17;
let A be non empty convex Subset of (TOP-REAL n); :: thesis: ( A is compact & not A is boundary implies 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 )
assume A4: ( A is compact & not A is boundary ) ; :: thesis: 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
A5: ( [#] ((TOP-REAL n) | A) = A & Fr A c= A ) by A4, PRE_TOPC:def 5, TOPS_1:35;
let FR be non empty SubSpace of (TOP-REAL n) | A; :: thesis: ( [#] FR = Fr A implies not FR is_a_retract_of (TOP-REAL n) | A )
assume A6: [#] FR = Fr A ; :: thesis: not FR is_a_retract_of (TOP-REAL n) | A
n > 0

proof

assume n <= 0 ; :: thesis: contradiction
then n = 0 ;
then {(0. (TOP-REAL n))} = the carrier of (TOP-REAL n) by EUCLID:22, JORDAN2C:105;
then A7: A = [#] (TOP-REAL n) by ZFMISC_1:33;
then Fr A = (Cl A) \ A by TOPS_1:42;
hence contradiction by A6, A7, XBOOLE_1:37; :: thesis: verum

end;

then reconsider Ts = ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) | s as non empty SubSpace of (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) ;
assume FR is_a_retract_of (TOP-REAL n) | A ; :: thesis: contradiction
then consider F being continuous Function of ((TOP-REAL n) | A),FR such that
A8: F is being_a_retraction by BORSUK_1:def 17;
reconsider f = F as Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) by A6, A5, FUNCT_2:7;
A9: f is continuous by PRE_TOPC:26;
A10: rng F c= Fr A by A6;
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set TN = TOP-REAL N;
A11: [#] ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) = Sphere ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;
( (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) = Tdisk ((0. (TOP-REAL N)),1) & (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)) = Tcircle ((0. (TOP-REAL N)),1) ) by TOPREALB:def 6;
then A12: not Ts is_a_retract_of (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) by A3, Lm6;
not cl_Ball ((0. (TOP-REAL n)),1) is boundary by Lm5;
then consider h being Function of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))),((TOP-REAL n) | A) such that
A13: h is being_homeomorphism and
A14: h .: (Fr (cl_Ball ((0. (TOP-REAL n)),1))) = Fr A by A1, A4, Th7;
A15: dom h = [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A13, TOPS_2:def 5;
rng ((h ") * f) = ((h ") * f) .: (dom ((h ") * f)) by RELAT_1:113;
then A16: rng ((h ") * f) c= ((h ") * f) .: (dom f) by RELAT_1:25, RELAT_1:123;
reconsider H = h as Function ;
A17: Fr (cl_Ball ((0. (TOP-REAL n)),1)) = Sphere ((0. (TOP-REAL n)),1) by Th5;
rng h = [#] ((TOP-REAL n) | A) by A13, TOPS_2:def 5;
then A19: (h ") .: (Fr A) = h " (Fr A) by A13, A5, TOPS_2:55
.= Fr (cl_Ball ((0. (TOP-REAL n)),1)) by A13, A14, A2, A15, FUNCT_1:94, TOPS_1:35 ;
((h ") * f) .: (dom f) = (h ") .: (f .: (dom f)) by RELAT_1:126
.= (h ") .: (rng f) by RELAT_1:113 ;
then ((h ") * f) .: (dom f) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) by A19, A10, RELAT_1:123;
then ( rng (((h ") * f) * h) c= rng ((h ") * f) & rng ((h ") * f) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) ) by A16, RELAT_1:26, XBOOLE_1:1;
then rng (((h ") * f) * h) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) by XBOOLE_1:1;
then reconsider hfh = ((h ") * f) * h as Function of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))),Ts by A3, A17, A11, FUNCT_2:6;
h " is continuous by A13, TOPS_2:def 5;
then hfh is continuous by A13, A9, PRE_TOPC:27;
then not hfh is being_a_retraction by A12, BORSUK_1:def 17;
then consider x being Point of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) such that
A20: x in Sphere ((0. (TOP-REAL n)),1) and
A21: hfh . x <> x by A3, A11, BORSUK_1:def 16;
set hx = h . x;
A22: dom hfh = the carrier of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by FUNCT_2:def 1;
then A23: hfh . x = ((h ") * f) . (h . x) by FUNCT_1:12;
x in dom h by A22, FUNCT_1:11;
then A24: h . x in the carrier of FR by A6, A14, A17, A20, FUNCT_1:def 6;
h . x in dom ((h ") * f) by A22, FUNCT_1:11;
then A25: ((h ") * f) . (h . x) = (h ") . (f . (h . x)) by FUNCT_1:12;
A26: H " = h " by A13, TOPS_2:def 4;
(H ") . (h . x) = x by A13, A15, FUNCT_1:34;
hence contradiction by A8, A26, A21, A23, A25, A24, BORSUK_1:def 16; :: thesis: verum