let r be positive Real; :: thesis: for o being Point of ()
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 (); :: 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)
set y0 = the Point of Y;
set X = Tdisk (o,r);
A2: the Point of Y in the carrier of Y ;
( the carrier of (Tcircle (o,r)) = Sphere (o,r) & Sphere (o,r) c= cl_Ball (o,r) ) by ;
then reconsider x0 = the Point of Y as Point of (Tdisk (o,r)) by A1, A2, Th3;
reconsider a0 = 0 , a1 = 1 as Point of I by ;
set C = the constant Loop of x0;
A3: the constant Loop of x0 = I --> x0 by BORSUK_2:5
.= the carrier of I --> the Point of Y ;
then reconsider D = the constant Loop of x0 as Function of I,Y ;
A4: ( D = I --> the Point of Y & D . a0 = the Point of Y ) by ;
( the Point of Y, the Point of Y are_connected & D . a1 = the Point of Y ) by ;
then reconsider D = D as constant Loop of the Point of Y by ;
given R being continuous Function of (Tdisk (o,r)),Y such that A5: R is being_a_retraction ; :: according to BORSUK_1:def 17 :: thesis: contradiction
the carrier of (pi_1 (Y, the Point of Y)) = {(Class ((EqRel (Y, the Point of Y)),D))}
proof
set E = EqRel (Y, the Point of Y);
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(Class ((EqRel (Y, the Point of Y)),D))} c= the carrier of (pi_1 (Y, the Point of Y))
let x be object ; :: thesis: ( x in the carrier of (pi_1 (Y, the Point of Y)) implies x in {(Class ((EqRel (Y, the Point of Y)),D))} )
assume x in the carrier of (pi_1 (Y, the Point of Y)) ; :: thesis: x in {(Class ((EqRel (Y, the Point of Y)),D))}
then consider f0 being Loop of the Point of Y such that
A6: x = Class ((EqRel (Y, the Point of Y)),f0) by TOPALG_1:47;
reconsider g0 = f0 as Loop of x0 by TOPALG_2:1;
g0, the constant Loop of x0 are_homotopic by TOPALG_2:2;
then consider f being Function of ,(Tdisk (o,r)) such that
A7: f is continuous and
A8: for s being Point of I holds
( f . (s,0) = g0 . s & f . (s,1) = the constant Loop of x0 . s & ( for t being Point of I holds
( f . (0,t) = x0 & f . (1,t) = x0 ) ) ) ;
f0,D are_homotopic
proof
take F = R * f; :: according to BORSUK_2:def 7 :: thesis: ( F is continuous & ( for b1 being Element of the carrier of K543() holds
( F . (b1,0) = f0 . b1 & F . (b1,1) = D . b1 & F . (0,b1) = the Point of Y & F . (1,b1) = the Point of Y ) ) )

thus F is continuous by A7; :: thesis: for b1 being Element of the carrier of K543() holds
( F . (b1,0) = f0 . b1 & F . (b1,1) = D . b1 & F . (0,b1) = the Point of Y & F . (1,b1) = the Point of Y )

let s be Point of I; :: thesis: ( F . (s,0) = f0 . s & F . (s,1) = D . s & F . (0,s) = the Point of Y & F . (1,s) = the Point of Y )
thus F . (s,0) = F . [s,a0]
.= R . (f . (s,0)) by FUNCT_2:15
.= R . (g0 . s) by A8
.= f0 . s by A5 ; :: thesis: ( F . (s,1) = D . s & F . (0,s) = the Point of Y & F . (1,s) = the Point of Y )
thus F . (s,1) = F . [s,a1]
.= R . (f . (s,1)) by FUNCT_2:15
.= R . ( the constant Loop of x0 . s) by A8
.= D . s by A5 ; :: thesis: ( F . (0,s) = the Point of Y & F . (1,s) = the Point of Y )
thus F . (0,s) = F . [a0,s]
.= R . (f . (0,s)) by FUNCT_2:15
.= R . x0 by A8
.= the Point of Y by A5 ; :: thesis: F . (1,s) = the Point of Y
thus F . (1,s) = F . [a1,s]
.= R . (f . (1,s)) by FUNCT_2:15
.= R . x0 by A8
.= the Point of Y by A5 ; :: thesis: verum
end;
then x = Class ((EqRel (Y, the Point of Y)),D) by ;
hence x in {(Class ((EqRel (Y, the Point of Y)),D))} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Class ((EqRel (Y, the Point of Y)),D))} or x in the carrier of (pi_1 (Y, the Point of Y)) )
assume x in {(Class ((EqRel (Y, the Point of Y)),D))} ; :: thesis: x in the carrier of (pi_1 (Y, the Point of Y))
then A9: x = Class ((EqRel (Y, the Point of Y)),D) by TARSKI:def 1;
D in Loops the Point of Y by TOPALG_1:def 1;
then x in Class (EqRel (Y, the Point of Y)) by ;
hence x in the carrier of (pi_1 (Y, the Point of Y)) by TOPALG_1:def 5; :: thesis: verum
end;
hence contradiction by A1; :: thesis: verum