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))}

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

hence
contradiction
by A1; :: thesis: verum
set E = EqRel (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;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 ; :: 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)) )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

hence x in {(Class ((EqRel (Y, the Point of Y)),D))} by TARSKI:def 1; :: thesis: verum

end;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

then
x = Class ((EqRel (Y, the Point of Y)),D)
by A6, TOPALG_1:46;
take F = R * f; :: according to BORSUK_2:def 7 :: thesis: ( F is continuous & ( for b_{1} being Element of the carrier of K540() holds

( F . (b_{1},0) = f0 . b_{1} & F . (b_{1},1) = D . b_{1} & F . (0,b_{1}) = the Point of Y & F . (1,b_{1}) = the Point of Y ) ) )

thus F is continuous by A7; :: thesis: for b_{1} being Element of the carrier of K540() holds

( F . (b_{1},0) = f0 . b_{1} & F . (b_{1},1) = D . b_{1} & F . (0,b_{1}) = the Point of Y & F . (1,b_{1}) = 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;( F . (b

thus F is continuous by A7; :: thesis: for b

( F . (b

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

hence x in {(Class ((EqRel (Y, the Point of Y)),D))} by TARSKI:def 1; :: thesis: verum

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