:: BORSUK_6 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

scheme :: BORSUK_6:sch 1
ExFunc3CondD{ F1() -> non empty set , P1[ set ], P2[ set ], P3[ set ], F2( set ) -> set , F3( set ) -> set , F4( set ) -> set } :
ex f being Function st
( dom f = F1() & ( for c being Element of F1() holds
( ( P1[c] implies f . c = F2(c) ) & ( P2[c] implies f . c = F3(c) ) & ( P3[c] implies f . c = F4(c) ) ) ) )
provided
A1: for c being Element of F1() holds
( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P2[c] implies not P3[c] ) ) and
A2: for c being Element of F1() holds
( P1[c] or P2[c] or P3[c] )
proof end;

registration
let n be Nat;
cluster TOP-REAL n -> constituted-FinSeqs ;
coherence
TOP-REAL n is constituted-FinSeqs
proof end;
end;

theorem Th1: :: BORSUK_6:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the carrier of [:I[01] ,I[01] :] = [:[.0,1.],[.0,1.]:] by BORSUK_1:83, BORSUK_1:def 5;

Lm1: for x, b, c, d being complex number holds (((d - c) / b) * x) + c = ((1 - (x / b)) * c) + ((x / b) * d)
by XCMPLX_1:236;

theorem :: BORSUK_6:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: BORSUK_6:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: BORSUK_6:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: BORSUK_6:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, x being real number st a <= x & x <= b holds
(x - a) / (b - a) in the carrier of (Closed-Interval-TSpace 0,1)
proof end;

theorem Th6: :: BORSUK_6:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of I[01] st x <= 1 / 2 holds
2 * x is Point of I[01]
proof end;

theorem Th7: :: BORSUK_6:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of I[01] st x >= 1 / 2 holds
(2 * x) - 1 is Point of I[01]
proof end;

theorem Th8: :: BORSUK_6:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of I[01] holds p * q is Point of I[01]
proof end;

theorem Th9: :: BORSUK_6:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of I[01] holds (1 / 2) * x is Point of I[01]
proof end;

theorem Th10: :: BORSUK_6:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of I[01] st x >= 1 / 2 holds
x - (1 / 4) is Point of I[01]
proof end;

theorem :: BORSUK_6:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th12: :: BORSUK_6:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
id I[01] is Path of 0[01] , 1[01]
proof end;

theorem Th13: :: BORSUK_6:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being Point of I[01] st a <= b & c <= d holds
[:[.a,b.],[.c,d.]:] is non empty compact Subset of [:I[01] ,I[01] :]
proof end;

theorem Th14: :: BORSUK_6:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 <= (2 * (p `1 )) - 1 } & T = { p where p is Point of (TOP-REAL 2) : p `2 <= p `1 } holds
(AffineMap 1,0,(1 / 2),(1 / 2)) .: S = T
proof end;

theorem Th15: :: BORSUK_6:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 >= (2 * (p `1 )) - 1 } & T = { p where p is Point of (TOP-REAL 2) : p `2 >= p `1 } holds
(AffineMap 1,0,(1 / 2),(1 / 2)) .: S = T
proof end;

theorem Th16: :: BORSUK_6:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 >= 1 - (2 * (p `1 )) } & T = { p where p is Point of (TOP-REAL 2) : p `2 >= - (p `1 ) } holds
(AffineMap 1,0,(1 / 2),(- (1 / 2))) .: S = T
proof end;

theorem Th17: :: BORSUK_6:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 <= 1 - (2 * (p `1 )) } & T = { p where p is Point of (TOP-REAL 2) : p `2 <= - (p `1 ) } holds
(AffineMap 1,0,(1 / 2),(- (1 / 2))) .: S = T
proof end;

definition
let T be 1-sorted ;
attr T is real-membered means :Def1: :: BORSUK_6:def 1
the carrier of T is real-membered;
end;

:: deftheorem Def1 defines real-membered BORSUK_6:def 1 :
for T being 1-sorted holds
( T is real-membered iff the carrier of T is real-membered );

theorem Th18: :: BORSUK_6:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty 1-sorted holds
( T is real-membered iff for x being Element of T holds x is real )
proof end;

registration
cluster I[01] -> real-membered ;
coherence
I[01] is real-membered
proof end;
end;

registration
cluster non empty real-membered 1-sorted ;
existence
ex b1 being 1-sorted st
( not b1 is empty & b1 is real-membered )
proof end;
cluster non empty real-membered TopStruct ;
existence
ex b1 being TopSpace st
( not b1 is empty & b1 is real-membered )
proof end;
end;

registration
let T be real-membered 1-sorted ;
cluster -> real Element of the carrier of T;
coherence
for b1 being Element of T holds b1 is real
proof end;
end;

registration
let T be real-membered TopStruct ;
cluster -> real-membered SubSpace of T;
coherence
for b1 being SubSpace of T holds b1 is real-membered
proof end;
end;

registration
let S, T be non empty real-membered TopSpace;
let p be Element of [:S,T:];
cluster p `1 -> real ;
coherence
p `1 is real
proof end;
cluster p `2 -> real ;
coherence
p `2 is real
proof end;
end;

registration
let T be non empty SubSpace of [:I[01] ,I[01] :];
let x be Point of T;
cluster x `1 -> real ;
coherence
x `1 is real
proof end;
cluster x `2 -> real ;
coherence
x `2 is real
proof end;
end;

registration
cluster R^1 -> real-membered ;
coherence
R^1 is real-membered
proof end;
end;

theorem Th19: :: BORSUK_6:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{ p where p is Point of (TOP-REAL 2) : p `2 <= (2 * (p `1 )) - 1 } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th20: :: BORSUK_6:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{ p where p is Point of (TOP-REAL 2) : p `2 >= (2 * (p `1 )) - 1 } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th21: :: BORSUK_6:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{ p where p is Point of (TOP-REAL 2) : p `2 <= 1 - (2 * (p `1 )) } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th22: :: BORSUK_6:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{ p where p is Point of (TOP-REAL 2) : p `2 >= 1 - (2 * (p `1 )) } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th23: :: BORSUK_6:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{ p where p is Point of (TOP-REAL 2) : ( p `2 >= 1 - (2 * (p `1 )) & p `2 >= (2 * (p `1 )) - 1 ) } is closed Subset of (TOP-REAL 2)
proof end;

theorem Th24: :: BORSUK_6:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex f being Function of [:R^1 ,R^1 :],(TOP-REAL 2) st
for x, y being Real holds f . [x,y] = <*x,y*>
proof end;

theorem Th25: :: BORSUK_6:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{ p where p is Point of [:R^1 ,R^1 :] : p `2 <= 1 - (2 * (p `1 )) } is closed Subset of [:R^1 ,R^1 :]
proof end;

theorem Th26: :: BORSUK_6:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{ p where p is Point of [:R^1 ,R^1 :] : p `2 <= (2 * (p `1 )) - 1 } is closed Subset of [:R^1 ,R^1 :]
proof end;

theorem Th27: :: BORSUK_6:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{ p where p is Point of [:R^1 ,R^1 :] : ( p `2 >= 1 - (2 * (p `1 )) & p `2 >= (2 * (p `1 )) - 1 ) } is closed Subset of [:R^1 ,R^1 :]
proof end;

theorem Th28: :: BORSUK_6:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{ p where p is Point of [:I[01] ,I[01] :] : p `2 <= 1 - (2 * (p `1 )) } is non empty closed Subset of [:I[01] ,I[01] :]
proof end;

theorem Th29: :: BORSUK_6:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{ p where p is Point of [:I[01] ,I[01] :] : ( p `2 >= 1 - (2 * (p `1 )) & p `2 >= (2 * (p `1 )) - 1 ) } is non empty closed Subset of [:I[01] ,I[01] :]
proof end;

theorem Th30: :: BORSUK_6:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{ p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 } is non empty closed Subset of [:I[01] ,I[01] :]
proof end;

theorem Th31: :: BORSUK_6:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace
for p being Point of [:S,T:] holds
( p `1 is Point of S & p `2 is Point of T )
proof end;

theorem Th32: :: BORSUK_6:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Subset of [:I[01] ,I[01] :] st A = [:[.0,(1 / 2).],[.0,1.]:] & B = [:[.(1 / 2),1.],[.0,1.]:] holds
([#] ([:I[01] ,I[01] :] | A)) \/ ([#] ([:I[01] ,I[01] :] | B)) = [#] [:I[01] ,I[01] :]
proof end;

theorem Th33: :: BORSUK_6:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Subset of [:I[01] ,I[01] :] st A = [:[.0,(1 / 2).],[.0,1.]:] & B = [:[.(1 / 2),1.],[.0,1.]:] holds
([#] ([:I[01] ,I[01] :] | A)) /\ ([#] ([:I[01] ,I[01] :] | B)) = [:{(1 / 2)},[.0,1.]:]
proof end;

registration
let T be TopStruct ;
cluster {} T -> compact ;
coherence
{} T is compact
by COMPTS_1:9;
end;

registration
let T be TopStruct ;
cluster empty compact Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( b1 is empty & b1 is compact )
proof end;
end;

theorem Th34: :: BORSUK_6:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct holds {} is empty compact Subset of T
proof end;

theorem Th35: :: BORSUK_6:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct
for a, b being real number st a > b holds
[.a,b.] is empty compact Subset of T
proof end;

theorem :: BORSUK_6:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being Point of I[01] holds [:[.a,b.],[.c,d.]:] is compact Subset of [:I[01] ,I[01] :]
proof end;

definition
let a, b, c, d be real number ;
func L[01] a,b,c,d -> Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d) equals :: BORSUK_6:def 2
(L[01] ((#) c,d),(c,d (#) )) * (P[01] a,b,((#) 0,1),(0,1 (#) ));
correctness
coherence
(L[01] ((#) c,d),(c,d (#) )) * (P[01] a,b,((#) 0,1),(0,1 (#) )) is Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d)
;
;
end;

:: deftheorem defines L[01] BORSUK_6:def 2 :
for a, b, c, d being real number holds L[01] a,b,c,d = (L[01] ((#) c,d),(c,d (#) )) * (P[01] a,b,((#) 0,1),(0,1 (#) ));

theorem Th37: :: BORSUK_6:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being real number st a < b & c < d holds
( (L[01] a,b,c,d) . a = c & (L[01] a,b,c,d) . b = d )
proof end;

theorem Th38: :: BORSUK_6:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being real number st a < b & c <= d holds
L[01] a,b,c,d is continuous Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d)
proof end;

theorem Th39: :: BORSUK_6:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being real number st a < b & c <= d holds
for x being real number st a <= x & x <= b holds
(L[01] a,b,c,d) . x = (((d - c) / (b - a)) * (x - a)) + c
proof end;

theorem Th40: :: BORSUK_6:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being Function of [:I[01] ,I[01] :],I[01] st f1 is continuous & f2 is continuous & ( for p being Point of [:I[01] ,I[01] :] holds (f1 . p) * (f2 . p) is Point of I[01] ) holds
ex g being Function of [:I[01] ,I[01] :],I[01] st
( ( for p being Point of [:I[01] ,I[01] :]
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * r2 ) & g is continuous )
proof end;

theorem Th41: :: BORSUK_6:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being Function of [:I[01] ,I[01] :],I[01] st f1 is continuous & f2 is continuous & ( for p being Point of [:I[01] ,I[01] :] holds (f1 . p) + (f2 . p) is Point of I[01] ) holds
ex g being Function of [:I[01] ,I[01] :],I[01] st
( ( for p being Point of [:I[01] ,I[01] :]
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 + r2 ) & g is continuous )
proof end;

theorem :: BORSUK_6:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being Function of [:I[01] ,I[01] :],I[01] st f1 is continuous & f2 is continuous & ( for p being Point of [:I[01] ,I[01] :] holds (f1 . p) - (f2 . p) is Point of I[01] ) holds
ex g being Function of [:I[01] ,I[01] :],I[01] st
( ( for p being Point of [:I[01] ,I[01] :]
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 - r2 ) & g is continuous )
proof end;

theorem Th43: :: BORSUK_6:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b st P is continuous holds
P * (L[01] (0,1 (#) ),((#) 0,1)) is continuous Function of I[01] ,T
proof end;

theorem Th44: :: BORSUK_6:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopStruct
for a, b being Point of X
for P being Path of a,b st P . 0 = a & P . 1 = b holds
( (P * (L[01] (0,1 (#) ),((#) 0,1))) . 0 = b & (P * (L[01] (0,1 (#) ),((#) 0,1))) . 1 = a )
proof end;

theorem Th45: :: BORSUK_6:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b st P is continuous & P . 0 = a & P . 1 = b holds
( - P is continuous & (- P) . 0 = b & (- P) . 1 = a )
proof end;

definition
let T be non empty TopSpace;
let a, b be Point of T;
:: original: are_connected
redefine pred a,b are_connected ;
reflexivity
for a being Point of T holds a,a are_connected
proof end;
symmetry
for a, b being Point of T st a,b are_connected holds
b,a are_connected
proof end;
end;

theorem Th46: :: BORSUK_6:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b, c being Point of T st a,b are_connected & b,c are_connected holds
a,c are_connected
proof end;

theorem :: BORSUK_6:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: BORSUK_6:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: BORSUK_6:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th50: :: BORSUK_6:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b being Point of T st a,b are_connected holds
for A being Path of a,b holds A = - (- A)
proof end;

theorem :: BORSUK_6:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty arcwise_connected TopSpace
for a, b being Point of T
for A being Path of a,b holds A = - (- A)
proof end;

definition
let T be non empty arcwise_connected TopSpace;
let a, b, c be Point of T;
let P be Path of a,b;
let Q be Path of b,c;
canceled;
redefine func P + Q means :: BORSUK_6:def 4
for t being Point of I[01] holds
( ( t <= 1 / 2 implies it . t = P . (2 * t) ) & ( 1 / 2 <= t implies it . t = Q . ((2 * t) - 1) ) );
compatibility
for b1 being Path of a,c holds
( b1 = P + Q iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b1 . t = Q . ((2 * t) - 1) ) ) )
proof end;
end;

:: deftheorem BORSUK_6:def 3 :
canceled;

:: deftheorem defines + BORSUK_6:def 4 :
for T being non empty arcwise_connected TopSpace
for a, b, c being Point of T
for P being Path of a,b
for Q being Path of b,c
for b7 being Path of a,c holds
( b7 = P + Q iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies b7 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b7 . t = Q . ((2 * t) - 1) ) ) );

definition
let T be non empty arcwise_connected TopSpace;
let a, b be Point of T;
let P be Path of a,b;
redefine func - P means :Def5: :: BORSUK_6:def 5
for t being Point of I[01] holds it . t = P . (1 - t);
compatibility
for b1 being Path of b,a holds
( b1 = - P iff for t being Point of I[01] holds b1 . t = P . (1 - t) )
proof end;
end;

:: deftheorem Def5 defines - BORSUK_6:def 5 :
for T being non empty arcwise_connected TopSpace
for a, b being Point of T
for P being Path of a,b
for b5 being Path of b,a holds
( b5 = - P iff for t being Point of I[01] holds b5 . t = P . (1 - t) );

definition
let T be non empty TopSpace;
let a, b be Point of T;
let P be Path of a,b;
let f be continuous Function of I[01] ,I[01] ;
assume A1: ( f . 0 = 0 & f . 1 = 1 & a,b are_connected ) ;
func RePar P,f -> Path of a,b equals :Def6: :: BORSUK_6:def 6
P * f;
coherence
P * f is Path of a,b
proof end;
end;

:: deftheorem Def6 defines RePar BORSUK_6:def 6 :
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b
for f being continuous Function of I[01] ,I[01] st f . 0 = 0 & f . 1 = 1 & a,b are_connected holds
RePar P,f = P * f;

theorem :: BORSUK_6:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th53: :: BORSUK_6:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b
for f being continuous Function of I[01] ,I[01] st f . 0 = 0 & f . 1 = 1 & a,b are_connected holds
RePar P,f,P are_homotopic
proof end;

theorem :: BORSUK_6:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty arcwise_connected TopSpace
for a, b being Point of T
for P being Path of a,b
for f being continuous Function of I[01] ,I[01] st f . 0 = 0 & f . 1 = 1 holds
RePar P,f,P are_homotopic
proof end;

definition
func 1RP -> Function of I[01] ,I[01] means :Def7: :: BORSUK_6:def 7
for t being Point of I[01] holds
( ( t <= 1 / 2 implies it . t = 2 * t ) & ( t > 1 / 2 implies it . t = 1 ) );
existence
ex b1 being Function of I[01] ,I[01] st
for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = 2 * t ) & ( t > 1 / 2 implies b1 . t = 1 ) )
proof end;
uniqueness
for b1, b2 being Function of I[01] ,I[01] st ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = 2 * t ) & ( t > 1 / 2 implies b1 . t = 1 ) ) ) & ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies b2 . t = 2 * t ) & ( t > 1 / 2 implies b2 . t = 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines 1RP BORSUK_6:def 7 :
for b1 being Function of I[01] ,I[01] holds
( b1 = 1RP iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = 2 * t ) & ( t > 1 / 2 implies b1 . t = 1 ) ) );

registration
cluster 1RP -> continuous ;
coherence
1RP is continuous
proof end;
end;

theorem Th55: :: BORSUK_6:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 1RP . 0 = 0 & 1RP . 1 = 1 )
proof end;

definition
func 2RP -> Function of I[01] ,I[01] means :Def8: :: BORSUK_6:def 8
for t being Point of I[01] holds
( ( t <= 1 / 2 implies it . t = 0 ) & ( t > 1 / 2 implies it . t = (2 * t) - 1 ) );
existence
ex b1 being Function of I[01] ,I[01] st
for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = 0 ) & ( t > 1 / 2 implies b1 . t = (2 * t) - 1 ) )
proof end;
uniqueness
for b1, b2 being Function of I[01] ,I[01] st ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = 0 ) & ( t > 1 / 2 implies b1 . t = (2 * t) - 1 ) ) ) & ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies b2 . t = 0 ) & ( t > 1 / 2 implies b2 . t = (2 * t) - 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines 2RP BORSUK_6:def 8 :
for b1 being Function of I[01] ,I[01] holds
( b1 = 2RP iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = 0 ) & ( t > 1 / 2 implies b1 . t = (2 * t) - 1 ) ) );

registration
cluster 2RP -> continuous ;
coherence
2RP is continuous
proof end;
end;

theorem Th56: :: BORSUK_6:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 2RP . 0 = 0 & 2RP . 1 = 1 )
proof end;

definition
func 3RP -> Function of I[01] ,I[01] means :Def9: :: BORSUK_6:def 9
for x being Point of I[01] holds
( ( x <= 1 / 2 implies it . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies it . x = x - (1 / 4) ) & ( x > 3 / 4 implies it . x = (2 * x) - 1 ) );
existence
ex b1 being Function of I[01] ,I[01] st
for x being Point of I[01] holds
( ( x <= 1 / 2 implies b1 . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies b1 . x = x - (1 / 4) ) & ( x > 3 / 4 implies b1 . x = (2 * x) - 1 ) )
proof end;
uniqueness
for b1, b2 being Function of I[01] ,I[01] st ( for x being Point of I[01] holds
( ( x <= 1 / 2 implies b1 . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies b1 . x = x - (1 / 4) ) & ( x > 3 / 4 implies b1 . x = (2 * x) - 1 ) ) ) & ( for x being Point of I[01] holds
( ( x <= 1 / 2 implies b2 . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies b2 . x = x - (1 / 4) ) & ( x > 3 / 4 implies b2 . x = (2 * x) - 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines 3RP BORSUK_6:def 9 :
for b1 being Function of I[01] ,I[01] holds
( b1 = 3RP iff for x being Point of I[01] holds
( ( x <= 1 / 2 implies b1 . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies b1 . x = x - (1 / 4) ) & ( x > 3 / 4 implies b1 . x = (2 * x) - 1 ) ) );

registration
cluster 3RP -> continuous ;
coherence
3RP is continuous
proof end;
end;

theorem Th57: :: BORSUK_6:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 3RP . 0 = 0 & 3RP . 1 = 1 )
proof end;

theorem Th58: :: BORSUK_6:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b
for Q being constant Path of b,b st a,b are_connected holds
RePar P,1RP = P + Q
proof end;

theorem Th59: :: BORSUK_6:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b
for Q being constant Path of a,a st a,b are_connected holds
RePar P,2RP = Q + P
proof end;

theorem Th60: :: BORSUK_6:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b, c, d being Point of T
for P being Path of a,b
for Q being Path of b,c
for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds
RePar ((P + Q) + R),3RP = P + (Q + R)
proof end;

definition
func LowerLeftUnitTriangle -> Subset of [:I[01] ,I[01] :] means :Def10: :: BORSUK_6:def 10
for x being set holds
( x in it iff ex a, b being Point of I[01] st
( x = [a,b] & b <= 1 - (2 * a) ) );
existence
ex b1 being Subset of [:I[01] ,I[01] :] st
for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= 1 - (2 * a) ) )
proof end;
uniqueness
for b1, b2 being Subset of [:I[01] ,I[01] :] st ( for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= 1 - (2 * a) ) ) ) & ( for x being set holds
( x in b2 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= 1 - (2 * a) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines LowerLeftUnitTriangle BORSUK_6:def 10 :
for b1 being Subset of [:I[01] ,I[01] :] holds
( b1 = LowerLeftUnitTriangle iff for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= 1 - (2 * a) ) ) );

notation
synonym IAA for LowerLeftUnitTriangle ;
end;

definition
func UpperUnitTriangle -> Subset of [:I[01] ,I[01] :] means :Def11: :: BORSUK_6:def 11
for x being set holds
( x in it iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) );
existence
ex b1 being Subset of [:I[01] ,I[01] :] st
for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) )
proof end;
uniqueness
for b1, b2 being Subset of [:I[01] ,I[01] :] st ( for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) ) & ( for x being set holds
( x in b2 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines UpperUnitTriangle BORSUK_6:def 11 :
for b1 being Subset of [:I[01] ,I[01] :] holds
( b1 = UpperUnitTriangle iff for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) );

notation
synonym IBB for UpperUnitTriangle ;
end;

definition
func LowerRightUnitTriangle -> Subset of [:I[01] ,I[01] :] means :Def12: :: BORSUK_6:def 12
for x being set holds
( x in it iff ex a, b being Point of I[01] st
( x = [a,b] & b <= (2 * a) - 1 ) );
existence
ex b1 being Subset of [:I[01] ,I[01] :] st
for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= (2 * a) - 1 ) )
proof end;
uniqueness
for b1, b2 being Subset of [:I[01] ,I[01] :] st ( for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= (2 * a) - 1 ) ) ) & ( for x being set holds
( x in b2 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= (2 * a) - 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines LowerRightUnitTriangle BORSUK_6:def 12 :
for b1 being Subset of [:I[01] ,I[01] :] holds
( b1 = LowerRightUnitTriangle iff for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= (2 * a) - 1 ) ) );

notation
synonym ICC for LowerRightUnitTriangle ;
end;

theorem Th61: :: BORSUK_6:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
IAA = { p where p is Point of [:I[01] ,I[01] :] : p `2 <= 1 - (2 * (p `1 )) }
proof end;

theorem Th62: :: BORSUK_6:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
IBB = { p where p is Point of [:I[01] ,I[01] :] : ( p `2 >= 1 - (2 * (p `1 )) & p `2 >= (2 * (p `1 )) - 1 ) }
proof end;

theorem Th63: :: BORSUK_6:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ICC = { p where p is Point of [:I[01] ,I[01] :] : p `2 <= (2 * (p `1 )) - 1 }
proof end;

registration
cluster LowerLeftUnitTriangle -> non empty closed ;
coherence
( IAA is closed & not IAA is empty )
by Th28, Th61;
cluster UpperUnitTriangle -> non empty closed ;
coherence
( IBB is closed & not IBB is empty )
by Th29, Th62;
cluster LowerRightUnitTriangle -> non empty closed ;
coherence
( ICC is closed & not ICC is empty )
by Th30, Th63;
end;

theorem Th64: :: BORSUK_6:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
(IAA \/ IBB ) \/ ICC = [:[.0,1.],[.0,1.]:]
proof end;

theorem Th65: :: BORSUK_6:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
IAA /\ IBB = { p where p is Point of [:I[01] ,I[01] :] : p `2 = 1 - (2 * (p `1 )) }
proof end;

theorem Th66: :: BORSUK_6:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ICC /\ IBB = { p where p is Point of [:I[01] ,I[01] :] : p `2 = (2 * (p `1 )) - 1 }
proof end;

theorem Th67: :: BORSUK_6:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of [:I[01] ,I[01] :] st x in IAA holds
x `1 <= 1 / 2
proof end;

theorem Th68: :: BORSUK_6:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of [:I[01] ,I[01] :] st x in ICC holds
x `1 >= 1 / 2
proof end;

theorem Th69: :: BORSUK_6:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of I[01] holds [0,x] in IAA
proof end;

theorem Th70: :: BORSUK_6:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being set st [0,s] in IBB holds
s = 1
proof end;

theorem Th71: :: BORSUK_6:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being set st [s,1] in ICC holds
s = 1
proof end;

theorem Th72: :: BORSUK_6:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
[0,1] in IBB
proof end;

theorem Th73: :: BORSUK_6:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of I[01] holds [x,1] in IBB
proof end;

theorem Th74: :: BORSUK_6:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( [(1 / 2),0] in ICC & [1,1] in ICC )
proof end;

theorem Th75: :: BORSUK_6:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
[(1 / 2),0] in IBB
proof end;

theorem Th76: :: BORSUK_6:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of I[01] holds [1,x] in ICC
proof end;

theorem Th77: :: BORSUK_6:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of I[01] st x >= 1 / 2 holds
[x,0] in ICC
proof end;

theorem Th78: :: BORSUK_6:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of I[01] st x <= 1 / 2 holds
[x,0] in IAA
proof end;

theorem Th79: :: BORSUK_6:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Point of I[01] st x < 1 / 2 holds
( not [x,0] in IBB & not [x,0] in ICC )
proof end;

theorem Th80: :: BORSUK_6:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
IAA /\ ICC = {[(1 / 2),0]}
proof end;

Lm2: for x, y being Point of I[01] holds [x,y] in the carrier of [:I[01] ,I[01] :]
;

theorem Th81: :: BORSUK_6:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b, c, d being Point of T
for P being Path of a,b
for Q being Path of b,c
for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds
(P + Q) + R,P + (Q + R) are_homotopic
proof end;

theorem :: BORSUK_6:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty arcwise_connected TopSpace
for a1, b1, c1, d1 being Point of X
for P being Path of a1,b1
for Q being Path of b1,c1
for R being Path of c1,d1 holds (P + Q) + R,P + (Q + R) are_homotopic
proof end;

theorem Th83: :: BORSUK_6:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b, c being Point of T
for P1, P2 being Path of a,b
for Q1, Q2 being Path of b,c st a,b are_connected & b,c are_connected & P1,P2 are_homotopic & Q1,Q2 are_homotopic holds
P1 + Q1,P2 + Q2 are_homotopic
proof end;

theorem :: BORSUK_6:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty arcwise_connected TopSpace
for a1, b1, c1 being Point of X
for P1, P2 being Path of a1,b1
for Q1, Q2 being Path of b1,c1 st P1,P2 are_homotopic & Q1,Q2 are_homotopic holds
P1 + Q1,P2 + Q2 are_homotopic
proof end;

theorem Th85: :: BORSUK_6:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b being Point of T
for P, Q being Path of a,b st a,b are_connected & P,Q are_homotopic holds
- P, - Q are_homotopic
proof end;

theorem :: BORSUK_6:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty arcwise_connected TopSpace
for a1, b1 being Point of X
for P, Q being Path of a1,b1 st P,Q are_homotopic holds
- P, - Q are_homotopic
proof end;

theorem :: BORSUK_6:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b being Point of T
for P, Q, R being Path of a,b st P,Q are_homotopic & Q,R are_homotopic holds
P,R are_homotopic
proof end;

theorem Th88: :: BORSUK_6:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b
for Q being constant Path of b,b st a,b are_connected holds
P + Q,P are_homotopic
proof end;

theorem :: BORSUK_6:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty arcwise_connected TopSpace
for a1, b1 being Point of X
for P being Path of a1,b1
for Q being constant Path of b1,b1 holds P + Q,P are_homotopic
proof end;

theorem Th90: :: BORSUK_6:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b
for Q being constant Path of a,a st a,b are_connected holds
Q + P,P are_homotopic
proof end;

theorem :: BORSUK_6:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty arcwise_connected TopSpace
for a1, b1 being Point of X
for P being Path of a1,b1
for Q being constant Path of a1,a1 holds Q + P,P are_homotopic
proof end;

theorem Th92: :: BORSUK_6:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b
for Q being constant Path of a,a st a,b are_connected holds
P + (- P),Q are_homotopic
proof end;

theorem :: BORSUK_6:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty arcwise_connected TopSpace
for a1, b1 being Point of X
for P being Path of a1,b1
for Q being constant Path of a1,a1 holds P + (- P),Q are_homotopic
proof end;

theorem Th94: :: BORSUK_6:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for b, a being Point of T
for P being Path of b,a
for Q being constant Path of a,a st b,a are_connected holds
(- P) + P,Q are_homotopic
proof end;

theorem :: BORSUK_6:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty arcwise_connected TopSpace
for b1, a1 being Point of X
for P being Path of b1,a1
for Q being constant Path of a1,a1 holds (- P) + P,Q are_homotopic
proof end;

theorem :: BORSUK_6:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for a being Point of T
for P, Q being constant Path of a,a holds P,Q are_homotopic
proof end;

definition
let T be non empty TopSpace;
let a, b be Point of T;
let P, Q be Path of a,b;
assume A1: P,Q are_homotopic ;
mode Homotopy of P,Q -> Function of [:I[01] ,I[01] :],T means :: BORSUK_6:def 13
( it is continuous & ( for s being Point of I[01] holds
( it . s,0 = P . s & it . s,1 = Q . s & ( for t being Point of I[01] holds
( it . 0,t = a & it . 1,t = b ) ) ) ) );
existence
ex b1 being Function of [:I[01] ,I[01] :],T st
( b1 is continuous & ( for s being Point of I[01] holds
( b1 . s,0 = P . s & b1 . s,1 = Q . s & ( for t being Point of I[01] holds
( b1 . 0,t = a & b1 . 1,t = b ) ) ) ) )
by A1, BORSUK_2:def 7;
end;

:: deftheorem defines Homotopy BORSUK_6:def 13 :
for T being non empty TopSpace
for a, b being Point of T
for P, Q being Path of a,b st P,Q are_homotopic holds
for b6 being Function of [:I[01] ,I[01] :],T holds
( b6 is Homotopy of P,Q iff ( b6 is continuous & ( for s being Point of I[01] holds
( b6 . s,0 = P . s & b6 . s,1 = Q . s & ( for t being Point of I[01] holds
( b6 . 0,t = a & b6 . 1,t = b ) ) ) ) ) );