let r be positive Real; :: 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)
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 TOPREAL9:17, TOPREALB:9;
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[01] by BORSUK_1:def 14, BORSUK_1:def 15;
set C = the constant Loop of x0;
A3: the constant Loop of x0 = I[01] --> x0 by BORSUK_2:5
.= the carrier of I[01] --> the Point of Y ;
then reconsider D = the constant Loop of x0 as Function of I[01],Y ;
A4: ( D = I[01] --> the Point of Y & D . a0 = the Point of Y ) by A3, FUNCOP_1:7;
( the Point of Y, the Point of Y are_connected & D . a1 = the Point of Y ) by A3, FUNCOP_1:7;
then reconsider D = D as constant Loop of the Point of Y 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 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 [: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) = the constant Loop of x0 . s & ( for t being Point of I[01] 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 b₁ being Element of the carrier of K543() holds
( F . (b₁,0) = f0 . b₁ & F . (b₁,1) = D . b₁ & F . (0,b₁) = the Point of Y & F . (1,b₁) = the Point of Y ) ) )
thus F is continuous by A7; :: thesis: for b₁ being Element of the carrier of K543() holds
( F . (b₁,0) = f0 . b₁ & F . (b₁,1) = D . b₁ & F . (0,b₁) = the Point of Y & F . (1,b₁) = the Point of Y )
let s be Point of I[01]; :: 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 A6, TOPALG_1:46;
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 A9, EQREL_1:def 3;
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