let n be Element of NAT ; :: thesis: for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b holds P,Q are_homotopic
let T be non empty convex SubSpace of TOP-REAL n; :: thesis: for a, b being Point of T
for P, Q being Path of a,b holds P,Q are_homotopic
let a, b be Point of T; :: thesis: for P, Q being Path of a,b holds P,Q are_homotopic
let P, Q be Path of a,b; :: thesis: P,Q are_homotopic
take F = ConvexHomotopy (P,Q); :: according to BORSUK_2:def 7 :: thesis: ( F is continuous & ( for b₁ being Element of the carrier of I[01] holds
( F . (b₁,0) = P . b₁ & F . (b₁,1) = Q . b₁ & F . (0,b₁) = a & F . (1,b₁) = b ) ) )
thus F is continuous by Lm5; :: thesis: for b₁ being Element of the carrier of I[01] holds
( F . (b₁,0) = P . b₁ & F . (b₁,1) = Q . b₁ & F . (0,b₁) = a & F . (1,b₁) = b )
thus for b₁ being Element of the carrier of I[01] holds
( F . (b₁,0) = P . b₁ & F . (b₁,1) = Q . b₁ & F . (0,b₁) = a & F . (1,b₁) = b ) by Lm6; :: thesis: verum