let r be positive real number ; :: thesis: for o being Point of (TOP-REAL 2)
for Y being non empty SubSpace of Tdisk o,r st Y = Tcircle o,r holds
not Y is_a_retract_of Tdisk o,r
let o be Point of (TOP-REAL 2); :: thesis: for Y being non empty SubSpace of Tdisk o,r st Y = Tcircle o,r holds
not Y is_a_retract_of Tdisk o,r
let Y be non empty SubSpace of Tdisk o,r; :: thesis: ( Y = Tcircle o,r implies not Y is_a_retract_of Tdisk o,r )
assume A1: Y = Tcircle o,r ; :: thesis: not Y is_a_retract_of Tdisk o,r
consider y0 being Point of Y;
set X = Tdisk o,r;
A2: y0 in the carrier of Y ;
( the carrier of (Tcircle o,r) = Sphere o,r & Sphere o,r c= cl_Ball o,r ) by TOPREAL9:17, TOPREALB:9;
then reconsider x0 = y0 as Point of (Tdisk o,r) by A1, A2, Th3;
reconsider z0 = y0 as Point of (Tcircle o,r) by A1;
reconsider a0 = 0 , a1 = 1 as Point of I[01] by BORSUK_1:def 17, BORSUK_1:def 18;
consider C being constant Loop of x0;
A3: C = I[01] --> x0 by BORSUK_2:6
.= the carrier of I[01] --> y0 ;
then reconsider D = C as Function of I[01] ,Y ;
A4: ( D = I[01] --> y0 & D . a0 = y0 ) by A3, FUNCOP_1:13;
( y0,y0 are_connected & D . a1 = y0 ) by A3, FUNCOP_1:13;
then reconsider D = D as constant Loop of y0 by A4, BORSUK_2:def 2;
given R being continuous Function of (Tdisk o,r),Y such that A5: R is being_a_retraction ; :: according to BORSUK_1:def 20 :: thesis: contradiction
the carrier of (pi_1 Y,y0) = {(Class (EqRel Y,y0),D)}

proof

set E = EqRel Y,y0;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(Class (EqRel Y,y0),D)} c= the carrier of (pi_1 Y,y0)

let x be set ; :: thesis: ( x in the carrier of (pi_1 Y,y0) implies x in {(Class (EqRel Y,y0),D)} )
assume x in the carrier of (pi_1 Y,y0) ; :: thesis: x in {(Class (EqRel Y,y0),D)}
then consider f0 being Loop of y0 such that
A6: x = Class (EqRel Y,y0),f0 by TOPALG_1:48;
reconsider g0 = f0 as Loop of x0 by TOPALG_2:1;
g0,C are_homotopic by TOPALG_2:2;
then consider f being Function of [:I[01] ,I[01] :],(Tdisk o,r) such that
A7: f is continuous and
A8: for s being Point of I[01] holds
( f . s,0 = g0 . s & f . s,1 = C . s & ( for t being Point of I[01] holds
( f . 0 ,t = x0 & f . 1,t = x0 ) ) ) by BORSUK_2:def 7;
f0,D are_homotopic

proof

take F = R * f; :: according to BORSUK_2:def 7 :: thesis: ( F is continuous & ( for b₁ being Element of the carrier of K667() holds
( F . b₁,0 = f0 . b₁ & F . b₁,1 = D . b₁ & F . 0 ,b₁ = y0 & F . 1,b₁ = y0 ) ) )
thus F is continuous by A7; :: thesis: for b₁ being Element of the carrier of K667() holds
( F . b₁,0 = f0 . b₁ & F . b₁,1 = D . b₁ & F . 0 ,b₁ = y0 & F . 1,b₁ = y0 )
let s be Point of I[01] ; :: thesis: ( F . s,0 = f0 . s & F . s,1 = D . s & F . 0 ,s = y0 & F . 1,s = y0 )
thus F . s,0 = F . [s,a0]
.= R . (f . s,0 ) by FUNCT_2:21
.= R . (g0 . s) by A8
.= f0 . s by A5, BORSUK_1:def 19 ; :: thesis: ( F . s,1 = D . s & F . 0 ,s = y0 & F . 1,s = y0 )
thus F . s,1 = F . [s,a1]
.= R . (f . s,1) by FUNCT_2:21
.= R . (C . s) by A8
.= D . s by A5, BORSUK_1:def 19 ; :: thesis: ( F . 0 ,s = y0 & F . 1,s = y0 )
thus F . 0 ,s = F . [a0,s]
.= R . (f . 0 ,s) by FUNCT_2:21
.= R . x0 by A8
.= y0 by A5, BORSUK_1:def 19 ; :: thesis: F . 1,s = y0
thus F . 1,s = F . [a1,s]
.= R . (f . 1,s) by FUNCT_2:21
.= R . x0 by A8
.= y0 by A5, BORSUK_1:def 19 ; :: thesis: verum

end;

then x = Class (EqRel Y,y0),D by A6, TOPALG_1:47;
hence x in {(Class (EqRel Y,y0),D)} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Class (EqRel Y,y0),D)} or x in the carrier of (pi_1 Y,y0) )
assume x in {(Class (EqRel Y,y0),D)} ; :: thesis: x in the carrier of (pi_1 Y,y0)
then A9: x = Class (EqRel Y,y0),D by TARSKI:def 1;
D in Loops y0 by TOPALG_1:def 1;
then x in Class (EqRel Y,y0) by A9, EQREL_1:def 5;
hence x in the carrier of (pi_1 Y,y0) by TOPALG_1:def 5; :: thesis: verum

end;

hence contradiction by A1; :: thesis: verum