let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for S being Subset of (TOP-REAL n) st n >= 2 & S = ([#] (TOP-REAL n)) \ {p} holds
(TOP-REAL n) | S is pathwise_connected
let p be Point of (TOP-REAL n); :: thesis: for S being Subset of (TOP-REAL n) st n >= 2 & S = ([#] (TOP-REAL n)) \ {p} holds
(TOP-REAL n) | S is pathwise_connected
let S be Subset of (TOP-REAL n); :: thesis: ( n >= 2 & S = ([#] (TOP-REAL n)) \ {p} implies (TOP-REAL n) | S is pathwise_connected )
assume A1: n >= 2 ; :: thesis: ( not S = ([#] (TOP-REAL n)) \ {p} or (TOP-REAL n) | S is pathwise_connected )
assume A2: S = ([#] (TOP-REAL n)) \ {p} ; :: thesis: (TOP-REAL n) | S is pathwise_connected
then S is infinite by A1, RAMSEY_1:4;
then reconsider T = (TOP-REAL n) | S as non empty SubSpace of TOP-REAL n ;
A3: [#] T = ([#] (TOP-REAL n)) \ {p} by A2, PRE_TOPC:def 5;
A4: for a, b being Point of T
for a1, b1 being Point of (TOP-REAL n) st not p in LSeg (a1,b1) & a1 = a & b1 = b holds
a,b are_connected

proof

let a, b be Point of T; :: thesis: for a1, b1 being Point of (TOP-REAL n) st not p in LSeg (a1,b1) & a1 = a & b1 = b holds
a,b are_connected
let a1, b1 be Point of (TOP-REAL n); :: thesis: ( not p in LSeg (a1,b1) & a1 = a & b1 = b implies a,b are_connected )
assume A5: not p in LSeg (a1,b1) ; :: thesis: ( not a1 = a or not b1 = b or a,b are_connected )
assume A6: ( a1 = a & b1 = b ) ; :: thesis: a,b are_connected

per cases ( a1 <> b1 or a1 = b1 ) ;

suppose A7: a1 <> b1 ; :: thesis: a,b are_connected

A8: [#] ((TOP-REAL n) | (LSeg (a1,b1))) = LSeg (a1,b1) by PRE_TOPC:def 5;
A9: LSeg (a1,b1) c= ([#] (TOP-REAL n)) \ {p} by A5, ZFMISC_1:34;
reconsider Y = (TOP-REAL n) | (LSeg (a1,b1)) as non empty SubSpace of T by A3, A9, A8, RLTOPSP1:68, TSEP_1:4;
LSeg (a1,b1) is_an_arc_of a1,b1 by A7, TOPREAL1:9;
then consider h being Function of I[01],Y such that
A10: h is being_homeomorphism and
A11: ( h . 0 = a1 & h . 1 = b1 ) by TOPREAL1:def 1;
reconsider f = h as Function of I[01],T by A3, A9, A8, FUNCT_2:7;
take f ; :: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )
thus f is continuous by A10, PRE_TOPC:26; :: thesis: ( f . 0 = a & f . 1 = b )
thus ( f . 0 = a & f . 1 = b ) by A6, A11; :: thesis: verum

end;

suppose a1 = b1 ; :: thesis: a,b are_connected

hence a,b are_connected by A6; :: thesis: verum

end;

end;

end;

for a, b being Point of T holds a,b are_connected

proof

let a, b be Point of T; :: thesis: a,b are_connected
A12: the carrier of T is Subset of (TOP-REAL n) by TSEP_1:1;
( a in the carrier of T & b in the carrier of T ) ;
then reconsider a1 = a, b1 = b as Point of (TOP-REAL n) by A12;

per cases ( a1 <> b1 or a1 = b1 ) ;

suppose A13: a1 <> b1 ; :: thesis: a,b are_connected

per cases ( p in LSeg (a1,b1) or not p in LSeg (a1,b1) ) ;

suppose A14: p in LSeg (a1,b1) ; :: thesis: a,b are_connected

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
reconsider aa1 = a1, bb1 = b1 as Point of (TOP-REAL n1) ;
consider s being Real such that
A15: ( 0 <= s & s <= 1 & p = ((1 - s) * aa1) + (s * bb1) ) by A14, RLTOPSP1:76;
set q1 = b1 - a1;
reconsider k = n - 1 as Nat by A1, CHORD:1;
k + 1 > 1 by A1, XXREAL_0:2;
then A16: k >= 1 by NAT_1:13;
b1 - a1 <> 0. (TOP-REAL (k + 1)) by A13, RLVECT_1:21;
then TPlane ((b1 - a1),p) is k -manifold by MFOLD_2:30;
then [#] (TPlane ((b1 - a1),p)) is infinite by A16;
then [#] ((TOP-REAL n) | (Plane ((b1 - a1),p))) is infinite by MFOLD_2:def 3;
then A17: Plane ((b1 - a1),p) is infinite ;
reconsider X = Plane ((b1 - a1),p) as set ;
X \ {p} is infinite by A17, RAMSEY_1:4;
then consider x being object such that
A18: x in X \ {p} by XBOOLE_0:def 1;
A19: ( x in X & not x in {p} ) by A18, XBOOLE_0:def 5;
then x in { y where y is Point of (TOP-REAL n) : |((b1 - a1),(y - p))| = 0 } by MFOLD_2:def 2;
then consider c1 being Point of (TOP-REAL n) such that
A20: ( c1 = x & |((b1 - a1),(c1 - p))| = 0 ) ;
A21: |((b1 - a1),(b1 - a1))| <> 0

proof

assume |((b1 - a1),(b1 - a1))| = 0 ; :: thesis: contradiction
then b1 - a1 = 0. (TOP-REAL n) by EUCLID_2:41;
hence contradiction by A13, RLVECT_1:21; :: thesis: verum

end;

A22: not p in LSeg (a1,c1)

proof

assume A23: p in LSeg (a1,c1) ; :: thesis: contradiction
reconsider cc1 = c1 as Point of (TOP-REAL n1) ;
consider r being Real such that
A24: ( 0 <= r & r <= 1 & p = ((1 - r) * aa1) + (r * cc1) ) by A23, RLTOPSP1:76;
A25: 1 - r <> 0

proof

assume 1 - r = 0 ; :: thesis: contradiction
then p = (0. (TOP-REAL n)) + (1 * c1) by A24, RLVECT_1:10
.= (0. (TOP-REAL n)) + c1 by RLVECT_1:def 8
.= c1 by RLVECT_1:4 ;
hence contradiction by A19, A20, TARSKI:def 1; :: thesis: verum

end;

set q2 = c1 - a1;
c1 - p = (c1 - ((1 - r) * a1)) - (r * c1) by A24, RLVECT_1:27
.= (c1 + ((- (1 - r)) * a1)) - (r * c1) by RLVECT_1:79
.= (c1 + (((- 1) + r) * a1)) - (r * c1)
.= (c1 + (((- 1) * a1) + (r * a1))) - (r * c1) by RLVECT_1:def 6
.= (c1 + ((- a1) + (r * a1))) - (r * c1) by RLVECT_1:16
.= ((c1 + (- a1)) + (r * a1)) - (r * c1) by RLVECT_1:def 3
.= ((c1 - a1) + (r * a1)) + (r * (- c1)) by RLVECT_1:25
.= (c1 - a1) + ((r * a1) + (r * (- c1))) by RLVECT_1:def 3
.= (c1 - a1) + (r * (a1 + (- c1))) by RLVECT_1:def 5
.= (c1 - a1) + (r * (- (c1 - a1))) by RLVECT_1:33
.= (c1 - a1) + (- (r * (c1 - a1))) by RLVECT_1:25
.= (c1 - a1) + ((- r) * (c1 - a1)) by RLVECT_1:79
.= (1 * (c1 - a1)) + ((- r) * (c1 - a1)) by RLVECT_1:def 8
.= (1 + (- r)) * (c1 - a1) by RLVECT_1:def 6
.= (1 - r) * (c1 - a1) ;
then (1 - r) * |((b1 - a1),(c1 - a1))| = 0 by A20, EUCLID_2:20;
then A26: |((b1 - a1),(c1 - a1))| = 0 by A25, XCMPLX_1:6;
0. (TOP-REAL n) = (((1 - r) * a1) + (r * c1)) + (- (((1 - s) * a1) + (s * b1))) by A15, A24, RLVECT_1:5
.= (((1 - r) * a1) + (- (((1 - s) * a1) + (s * b1)))) + (r * c1) by RLVECT_1:def 3
.= (((1 - r) * a1) + ((- ((1 - s) * a1)) - (s * b1))) + (r * c1) by RLVECT_1:30
.= ((((1 - r) * a1) + (- ((1 - s) * a1))) + (- (s * b1))) + (r * c1) by RLVECT_1:def 3
.= ((((1 - r) * a1) + ((- (1 - s)) * a1)) + (- (s * b1))) + (r * c1) by RLVECT_1:79
.= ((((1 - r) + (- (1 - s))) * a1) + (- (s * b1))) + (r * c1) by RLVECT_1:def 6
.= (((s + (- r)) * a1) + (- (s * b1))) + (r * c1)
.= (((s * a1) + ((- r) * a1)) + (- (s * b1))) + (r * c1) by RLVECT_1:def 6
.= (((s * a1) + (- (s * b1))) + ((- r) * a1)) + (r * c1) by RLVECT_1:def 3
.= (((s * a1) + (s * (- b1))) + ((- r) * a1)) + (r * c1) by RLVECT_1:25
.= ((s * (a1 + (- b1))) + ((- r) * a1)) + (r * c1) by RLVECT_1:def 5
.= ((s * (- (b1 - a1))) + ((- r) * a1)) + (r * c1) by RLVECT_1:33
.= (s * (- (b1 - a1))) + (((- r) * a1) + (r * c1)) by RLVECT_1:def 3
.= (s * (- (b1 - a1))) + ((r * c1) + (- (r * a1))) by RLVECT_1:79
.= (s * (- (b1 - a1))) + ((r * c1) + (r * (- a1))) by RLVECT_1:25
.= (s * (- (b1 - a1))) + (r * (c1 - a1)) by RLVECT_1:def 5 ;
then A27: 0 = |(((s * (- (b1 - a1))) + (r * (c1 - a1))),((s * (- (b1 - a1))) + (r * (c1 - a1))))| by EUCLID_2:34
.= (|((s * (- (b1 - a1))),(s * (- (b1 - a1))))| + (2 * |((s * (- (b1 - a1))),(r * (c1 - a1)))|)) + |((r * (c1 - a1)),(r * (c1 - a1)))| by EUCLID_2:30 ;
A28: |((s * (- (b1 - a1))),(s * (- (b1 - a1))))| = s * |((- (b1 - a1)),(s * (- (b1 - a1))))| by EUCLID_2:19
.= s * (s * |((- (b1 - a1)),(- (b1 - a1)))|) by EUCLID_2:20
.= s * (s * |((b1 - a1),(b1 - a1))|) by EUCLID_2:23
.= (s * s) * |((b1 - a1),(b1 - a1))| ;
A29: |((r * (c1 - a1)),(r * (c1 - a1)))| = r * |((c1 - a1),(r * (c1 - a1)))| by EUCLID_2:19
.= r * (r * |((c1 - a1),(c1 - a1))|) by EUCLID_2:20
.= (r * r) * |((c1 - a1),(c1 - a1))| ;
A30: |((s * (- (b1 - a1))),(r * (c1 - a1)))| = s * |((- (b1 - a1)),(r * (c1 - a1)))| by EUCLID_2:19
.= s * (r * |((- (b1 - a1)),(c1 - a1))|) by EUCLID_2:20
.= s * (r * (- |((b1 - a1),(c1 - a1))|)) by EUCLID_2:21
.= 0 by A26 ;
A31: s * s >= 0 by XREAL_1:63;
A32: r * r >= 0 by XREAL_1:63;
A33: |((b1 - a1),(b1 - a1))| >= 0 by EUCLID_2:35;
A34: |((c1 - a1),(c1 - a1))| >= 0 by EUCLID_2:35;
A35: s * s <> 0

proof

assume s * s = 0 ; :: thesis: contradiction
then s = 0 by XCMPLX_1:6;
then p = (1 * a1) + (0. (TOP-REAL n)) by A15, RLVECT_1:10
.= 1 * a1 by RLVECT_1:4
.= a1 by RLVECT_1:def 8 ;
then not p in {p} by A3, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

thus contradiction by A28, A29, A27, A30, A31, A32, A33, A34, A35, A21, XREAL_1:71; :: thesis: verum

end;

A36: not p in LSeg (c1,b1)

proof

assume A37: p in LSeg (c1,b1) ; :: thesis: contradiction
reconsider cc1 = c1 as Point of (TOP-REAL n1) ;
consider r being Real such that
A38: ( 0 <= r & r <= 1 & p = ((1 - r) * bb1) + (r * cc1) ) by A37, RLTOPSP1:76;
A39: 1 - r <> 0

proof

assume 1 - r = 0 ; :: thesis: contradiction
then p = (0. (TOP-REAL n)) + (1 * c1) by A38, RLVECT_1:10
.= (0. (TOP-REAL n)) + c1 by RLVECT_1:def 8
.= c1 by RLVECT_1:4 ;
hence contradiction by A19, A20, TARSKI:def 1; :: thesis: verum

end;

set q2 = c1 - b1;
c1 - p = (c1 - ((1 - r) * b1)) - (r * c1) by A38, RLVECT_1:27
.= (c1 + ((- (1 - r)) * b1)) - (r * c1) by RLVECT_1:79
.= (c1 + (((- 1) + r) * b1)) - (r * c1)
.= (c1 + (((- 1) * b1) + (r * b1))) - (r * c1) by RLVECT_1:def 6
.= (c1 + ((- b1) + (r * b1))) - (r * c1) by RLVECT_1:16
.= ((c1 + (- b1)) + (r * b1)) - (r * c1) by RLVECT_1:def 3
.= ((c1 - b1) + (r * b1)) + (r * (- c1)) by RLVECT_1:25
.= (c1 - b1) + ((r * b1) + (r * (- c1))) by RLVECT_1:def 3
.= (c1 - b1) + (r * (b1 + (- c1))) by RLVECT_1:def 5
.= (c1 - b1) + (r * (- (c1 - b1))) by RLVECT_1:33
.= (c1 - b1) + (- (r * (c1 - b1))) by RLVECT_1:25
.= (c1 - b1) + ((- r) * (c1 - b1)) by RLVECT_1:79
.= (1 * (c1 - b1)) + ((- r) * (c1 - b1)) by RLVECT_1:def 8
.= (1 + (- r)) * (c1 - b1) by RLVECT_1:def 6
.= (1 - r) * (c1 - b1) ;
then (1 - r) * |((b1 - a1),(c1 - b1))| = 0 by A20, EUCLID_2:20;
then A40: |((b1 - a1),(c1 - b1))| = 0 by A39, XCMPLX_1:6;
A41: 0. (TOP-REAL n) = (((1 + (- r)) * b1) + (r * c1)) + (- (((1 - s) * a1) + (s * b1))) by A38, A15, RLVECT_1:5
.= (((1 * b1) + ((- r) * b1)) + (r * c1)) + (- (((1 - s) * a1) + (s * b1))) by RLVECT_1:def 6
.= ((b1 + ((- r) * b1)) + (r * c1)) + (- (((1 - s) * a1) + (s * b1))) by RLVECT_1:def 8
.= (b1 + (((- r) * b1) + (r * c1))) + (- (((1 - s) * a1) + (s * b1))) by RLVECT_1:def 3
.= (b1 + ((- (r * b1)) + (r * c1))) + (- (((1 - s) * a1) + (s * b1))) by RLVECT_1:79
.= (b1 + ((r * (- b1)) + (r * c1))) + (- (((1 - s) * a1) + (s * b1))) by RLVECT_1:25
.= (b1 + (r * (c1 - b1))) + (- (((1 - s) * a1) + (s * b1))) by RLVECT_1:def 5
.= (b1 + (- (((1 - s) * a1) + (s * b1)))) + (r * (c1 - b1)) by RLVECT_1:def 3
.= (b1 + ((- 1) * ((s * b1) + ((1 - s) * a1)))) + (r * (c1 - b1)) by RLVECT_1:16
.= (b1 + (((- 1) * (s * b1)) + ((- 1) * ((1 - s) * a1)))) + (r * (c1 - b1)) by RLVECT_1:def 5
.= (b1 + ((((- 1) * s) * b1) + ((- 1) * ((1 - s) * a1)))) + (r * (c1 - b1)) by RLVECT_1:def 7
.= (b1 + (((- s) * b1) + (- ((1 - s) * a1)))) + (r * (c1 - b1)) by RLVECT_1:16
.= ((b1 + ((- s) * b1)) + (- ((1 - s) * a1))) + (r * (c1 - b1)) by RLVECT_1:def 3
.= (((1 * b1) + ((- s) * b1)) + (- ((1 - s) * a1))) + (r * (c1 - b1)) by RLVECT_1:def 8
.= (((1 + (- s)) * b1) + (- ((1 - s) * a1))) + (r * (c1 - b1)) by RLVECT_1:def 6
.= (((1 - s) * b1) + ((1 - s) * (- a1))) + (r * (c1 - b1)) by RLVECT_1:25
.= ((1 - s) * (b1 - a1)) + (r * (c1 - b1)) by RLVECT_1:def 5 ;
set t = 1 - s;
A42: 0 = |((((1 - s) * (b1 - a1)) + (r * (c1 - b1))),(((1 - s) * (b1 - a1)) + (r * (c1 - b1))))| by A41, EUCLID_2:34
.= (|(((1 - s) * (b1 - a1)),((1 - s) * (b1 - a1)))| + (2 * |(((1 - s) * (b1 - a1)),(r * (c1 - b1)))|)) + |((r * (c1 - b1)),(r * (c1 - b1)))| by EUCLID_2:30 ;
A43: |(((1 - s) * (b1 - a1)),((1 - s) * (b1 - a1)))| = (1 - s) * |((b1 - a1),((1 - s) * (b1 - a1)))| by EUCLID_2:19
.= (1 - s) * ((1 - s) * |((b1 - a1),(b1 - a1))|) by EUCLID_2:20
.= ((1 - s) * (1 - s)) * |((b1 - a1),(b1 - a1))| ;
A44: |((r * (c1 - b1)),(r * (c1 - b1)))| = r * |((c1 - b1),(r * (c1 - b1)))| by EUCLID_2:19
.= r * (r * |((c1 - b1),(c1 - b1))|) by EUCLID_2:20
.= (r * r) * |((c1 - b1),(c1 - b1))| ;
A45: |(((1 - s) * (b1 - a1)),(r * (c1 - b1)))| = (1 - s) * |((b1 - a1),(r * (c1 - b1)))| by EUCLID_2:19
.= (1 - s) * (r * |((b1 - a1),(c1 - b1))|) by EUCLID_2:20
.= 0 by A40 ;
A46: (1 - s) * (1 - s) >= 0 by XREAL_1:63;
A47: r * r >= 0 by XREAL_1:63;
A48: |((b1 - a1),(b1 - a1))| >= 0 by EUCLID_2:35;
A49: |((c1 - b1),(c1 - b1))| >= 0 by EUCLID_2:35;
A50: (1 - s) * (1 - s) <> 0

proof

assume (1 - s) * (1 - s) = 0 ; :: thesis: contradiction
then 1 - s = 0 by XCMPLX_1:6;
then p = (0. (TOP-REAL n)) + (1 * b1) by A15, RLVECT_1:10
.= 1 * b1 by RLVECT_1:4
.= b1 by RLVECT_1:def 8 ;
then not p in {p} by A3, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

thus contradiction by A50, A21, A43, A44, A42, A45, A46, A47, A48, A49, XREAL_1:71; :: thesis: verum

end;

reconsider c = c1 as Point of T by A20, A19, A3, XBOOLE_0:def 5;
( a,c are_connected & c,b are_connected ) by A22, A36, A4;
hence a,b are_connected by BORSUK_6:42; :: thesis: verum

end;

suppose not p in LSeg (a1,b1) ; :: thesis: a,b are_connected

hence a,b are_connected by A4; :: thesis: verum

end;

end;

end;

suppose a1 = b1 ; :: thesis: a,b are_connected

hence a,b are_connected ; :: thesis: verum

end;

end;

end;

hence (TOP-REAL n) | S is pathwise_connected ; :: thesis: verum