:: JORDAN21 semantic presentation

begin

    Lm1:  dom proj2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def_1;

Lm2:  for r being real number
for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds
ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )
proof
let r be real number ; ::_thesis: for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds
ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )
let X be Subset of (TOP-REAL 2); ::_thesis: ( r in proj2 .: X implies ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r ) )
assume  r in proj2 .: X ; ::_thesis: ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )
then  ex x being set st
( x in the carrier of (TOP-REAL 2) & x in X & proj2 . x = r ) by FUNCT_2:64;
hence  ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r ) ; ::_thesis: verum
end;

Lm3: now__::_thesis:_for_a,_A,_B,_C_being_set_holds_
(_not_a_in_(A_\/_B)_\/_C_or_a_in_A_or_a_in_B_or_a_in_C_)
let a, A, B, C be set ; ::_thesis: ( not a in (A \/ B) \/ C or a in A or a in B or a in C )
assume  a in (A \/ B) \/ C ; ::_thesis: ( a in A or a in B or a in C )
then  ( a in A \/ B or a in C ) by XBOOLE_0:def_3;
hence  ( a in A or a in B or a in C ) by XBOOLE_0:def_3; ::_thesis: verum
end;

Lm4:  for A, B, C, D being set st A misses D & B misses D & C misses D holds
(A \/ B) \/ C misses D
proof
let A, B, C, D be set ; ::_thesis: ( A misses D & B misses D & C misses D implies (A \/ B) \/ C misses D )
assume  ( A misses D & B misses D ) ; ::_thesis: ( not C misses D or (A \/ B) \/ C misses D )
then A1: A \/ B misses D by XBOOLE_1:70;
assume  C misses D ; ::_thesis: (A \/ B) \/ C misses D
hence  (A \/ B) \/ C misses D by A1, XBOOLE_1:70; ::_thesis: verum
end;

theorem :: JORDAN21:1
for n being Element of NAT
for p being Point of (TOP-REAL n) holds {p} is bounded
proof
let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL n) holds {p} is bounded
let p be Point of (TOP-REAL n); ::_thesis: {p} is bounded
reconsider a = p as Point of (Euclid n) by EUCLID:67;
 {a} is bounded by TBSP_1:15;
hence  {p} is bounded by JORDAN2C:11; ::_thesis: verum
end;

theorem Th2: :: JORDAN21:2
for s1, t being real number
for P being Subset of (TOP-REAL 2) st P =  {  |[s,t]| where s is Real : s1 < s  }  holds
P is convex
proof
let s1, t be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P =  {  |[s,t]| where s is Real : s1 < s  }  holds
P is convex
let P be Subset of (TOP-REAL 2); ::_thesis: ( P =  {  |[s,t]| where s is Real : s1 < s  }  implies P is convex )
assume A1: P =  {  |[s,t]| where s is Real : s1 < s  }  ; ::_thesis: P is convex
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: ( not w1 in P or not w2 in P or LSeg (w1,w2) c= P )
assume that
A2: w1 in P and
A3: w2 in P ; ::_thesis: LSeg (w1,w2) c= P
consider s3 being Real such that
A4: |[s3,t]| = w1 and
A5: s1 < s3 by A1, A2;
consider s4 being Real such that
A6: |[s4,t]| = w2 and
A7: s1 < s4 by A1, A3;
A8: w2 `1 = s4 by A6, EUCLID:52;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg (w1,w2) or x in P )
assume  x in LSeg (w1,w2) ; ::_thesis: x in P
then consider l being Real such that
A9: x = ((1 - l) * w1) + (l * w2) and
A10: ( 0 <= l & l <= 1 ) ;
set w = ((1 - l) * w1) + (l * w2);
A11: ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) `1) + ((l * w2) `1)),((((1 - l) * w1) `2) + ((l * w2) `2))]| by EUCLID:55;
A12: l * w2 = |[(l * (w2 `1)),(l * (w2 `2))]| by EUCLID:57;
then A13: (l * w2) `1 = l * (w2 `1) by EUCLID:52;
A14: (1 - l) * w1 = |[((1 - l) * (w1 `1)),((1 - l) * (w1 `2))]| by EUCLID:57;
then  ((1 - l) * w1) `1 = (1 - l) * (w1 `1) by EUCLID:52;
then A15: (((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1)) + (l * (w2 `1)) by A11, A13, EUCLID:52;
A16: (l * w2) `2 = l * (w2 `2) by A12, EUCLID:52;
 ((1 - l) * w1) `2 = (1 - l) * (w1 `2) by A14, EUCLID:52;
then A17: (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2)) + (l * (w2 `2)) by A11, A16, EUCLID:52;
 w2 `2 = t by A6, EUCLID:52;
then A18: (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * t) + (l * t) by A4, A17, EUCLID:52
.= t - 0 ;
A19: ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) + (l * w2)) `1),((((1 - l) * w1) + (l * w2)) `2)]| by EUCLID:53;
 w1 `1 = s3 by A4, EUCLID:52;
then  s1 < (((1 - l) * w1) + (l * w2)) `1 by A5, A7, A8, A10, A15, XREAL_1:175;
hence  x in P by A1, A9, A19, A18; ::_thesis: verum
end;

theorem Th3: :: JORDAN21:3
for s2, t being real number
for P being Subset of (TOP-REAL 2) st P =  {  |[s,t]| where s is Real : s < s2  }  holds
P is convex
proof
let s2, t be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P =  {  |[s,t]| where s is Real : s < s2  }  holds
P is convex
let P be Subset of (TOP-REAL 2); ::_thesis: ( P =  {  |[s,t]| where s is Real : s < s2  }  implies P is convex )
assume A1: P =  {  |[s,t]| where s is Real : s < s2  }  ; ::_thesis: P is convex
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: ( not w1 in P or not w2 in P or LSeg (w1,w2) c= P )
assume that
A2: w1 in P and
A3: w2 in P ; ::_thesis: LSeg (w1,w2) c= P
consider s3 being Real such that
A4: |[s3,t]| = w1 and
A5: s3 < s2 by A1, A2;
consider s4 being Real such that
A6: |[s4,t]| = w2 and
A7: s4 < s2 by A1, A3;
A8: w2 `1 = s4 by A6, EUCLID:52;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg (w1,w2) or x in P )
assume  x in LSeg (w1,w2) ; ::_thesis: x in P
then consider l being Real such that
A9: x = ((1 - l) * w1) + (l * w2) and
A10: ( 0 <= l & l <= 1 ) ;
set w = ((1 - l) * w1) + (l * w2);
A11: ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) `1) + ((l * w2) `1)),((((1 - l) * w1) `2) + ((l * w2) `2))]| by EUCLID:55;
A12: l * w2 = |[(l * (w2 `1)),(l * (w2 `2))]| by EUCLID:57;
then A13: (l * w2) `1 = l * (w2 `1) by EUCLID:52;
A14: (1 - l) * w1 = |[((1 - l) * (w1 `1)),((1 - l) * (w1 `2))]| by EUCLID:57;
then  ((1 - l) * w1) `1 = (1 - l) * (w1 `1) by EUCLID:52;
then A15: (((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1)) + (l * (w2 `1)) by A11, A13, EUCLID:52;
A16: (l * w2) `2 = l * (w2 `2) by A12, EUCLID:52;
 ((1 - l) * w1) `2 = (1 - l) * (w1 `2) by A14, EUCLID:52;
then A17: (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2)) + (l * (w2 `2)) by A11, A16, EUCLID:52;
 w2 `2 = t by A6, EUCLID:52;
then A18: (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * t) + (l * t) by A4, A17, EUCLID:52
.= t - 0 ;
A19: ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) + (l * w2)) `1),((((1 - l) * w1) + (l * w2)) `2)]| by EUCLID:53;
 w1 `1 = s3 by A4, EUCLID:52;
then  s2 > (((1 - l) * w1) + (l * w2)) `1 by A5, A7, A8, A10, A15, XREAL_1:176;
hence  x in P by A1, A9, A19, A18; ::_thesis: verum
end;

theorem Th4: :: JORDAN21:4
for s, t1 being real number
for P being Subset of (TOP-REAL 2) st P =  {  |[s,t]| where t is Real : t1 < t  }  holds
P is convex
proof
let s, t1 be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P =  {  |[s,t]| where t is Real : t1 < t  }  holds
P is convex
let P be Subset of (TOP-REAL 2); ::_thesis: ( P =  {  |[s,t]| where t is Real : t1 < t  }  implies P is convex )
assume A1: P =  {  |[s,t]| where t is Real : t1 < t  }  ; ::_thesis: P is convex
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: ( not w1 in P or not w2 in P or LSeg (w1,w2) c= P )
assume that
A2: w1 in P and
A3: w2 in P ; ::_thesis: LSeg (w1,w2) c= P
consider t3 being Real such that
A4: |[s,t3]| = w1 and
A5: t1 < t3 by A1, A2;
A6: w1 `1 = s by A4, EUCLID:52;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg (w1,w2) or x in P )
assume  x in LSeg (w1,w2) ; ::_thesis: x in P
then consider l being Real such that
A7: x = ((1 - l) * w1) + (l * w2) and
A8: ( 0 <= l & l <= 1 ) ;
set w = ((1 - l) * w1) + (l * w2);
A9: ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) `1) + ((l * w2) `1)),((((1 - l) * w1) `2) + ((l * w2) `2))]| by EUCLID:55;
consider t4 being Real such that
A10: |[s,t4]| = w2 and
A11: t1 < t4 by A1, A3;
A12: w2 `1 = s by A10, EUCLID:52;
A13: l * w2 = |[(l * (w2 `1)),(l * (w2 `2))]| by EUCLID:57;
then A14: (l * w2) `1 = l * (w2 `1) by EUCLID:52;
A15: (l * w2) `2 = l * (w2 `2) by A13, EUCLID:52;
A16: (1 - l) * w1 = |[((1 - l) * (w1 `1)),((1 - l) * (w1 `2))]| by EUCLID:57;
then  ((1 - l) * w1) `2 = (1 - l) * (w1 `2) by EUCLID:52;
then A17: (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2)) + (l * (w2 `2)) by A9, A15, EUCLID:52;
A18: w2 `2 = t4 by A10, EUCLID:52;
 ((1 - l) * w1) `1 = (1 - l) * (w1 `1) by A16, EUCLID:52;
then A19: ( ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) + (l * w2)) `1),((((1 - l) * w1) + (l * w2)) `2)]| & (((1 - l) * w1) + (l * w2)) `1 = s - 0 ) by A6, A12, A9, A14, EUCLID:52, EUCLID:53;
 w1 `2 = t3 by A4, EUCLID:52;
then  t1 < (((1 - l) * w1) + (l * w2)) `2 by A5, A11, A18, A8, A17, XREAL_1:175;
hence  x in P by A1, A7, A19; ::_thesis: verum
end;

theorem Th5: :: JORDAN21:5
for s, t2 being real number
for P being Subset of (TOP-REAL 2) st P =  {  |[s,t]| where t is Real : t < t2  }  holds
P is convex
proof
let s, t2 be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P =  {  |[s,t]| where t is Real : t < t2  }  holds
P is convex
let P be Subset of (TOP-REAL 2); ::_thesis: ( P =  {  |[s,t]| where t is Real : t < t2  }  implies P is convex )
assume A1: P =  {  |[s,t]| where t is Real : t < t2  }  ; ::_thesis: P is convex
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: ( not w1 in P or not w2 in P or LSeg (w1,w2) c= P )
assume that
A2: w1 in P and
A3: w2 in P ; ::_thesis: LSeg (w1,w2) c= P
consider t3 being Real such that
A4: |[s,t3]| = w1 and
A5: t3 < t2 by A1, A2;
consider t4 being Real such that
A6: |[s,t4]| = w2 and
A7: t4 < t2 by A1, A3;
A8: w2 `2 = t4 by A6, EUCLID:52;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg (w1,w2) or x in P )
assume  x in LSeg (w1,w2) ; ::_thesis: x in P
then consider l being Real such that
A9: x = ((1 - l) * w1) + (l * w2) and
A10: ( 0 <= l & l <= 1 ) ;
set w = ((1 - l) * w1) + (l * w2);
A11: ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) `1) + ((l * w2) `1)),((((1 - l) * w1) `2) + ((l * w2) `2))]| by EUCLID:55;
A12: l * w2 = |[(l * (w2 `1)),(l * (w2 `2))]| by EUCLID:57;
then A13: (l * w2) `1 = l * (w2 `1) by EUCLID:52;
A14: (1 - l) * w1 = |[((1 - l) * (w1 `1)),((1 - l) * (w1 `2))]| by EUCLID:57;
then  ((1 - l) * w1) `1 = (1 - l) * (w1 `1) by EUCLID:52;
then A15: (((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1)) + (l * (w2 `1)) by A11, A13, EUCLID:52;
 w2 `1 = s by A6, EUCLID:52;
then A16: (((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * s) + (l * s) by A4, A15, EUCLID:52
.= s - 0 ;
A17: ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) + (l * w2)) `1),((((1 - l) * w1) + (l * w2)) `2)]| by EUCLID:53;
A18: (l * w2) `2 = l * (w2 `2) by A12, EUCLID:52;
 ((1 - l) * w1) `2 = (1 - l) * (w1 `2) by A14, EUCLID:52;
then A19: (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2)) + (l * (w2 `2)) by A11, A18, EUCLID:52;
 w1 `2 = t3 by A4, EUCLID:52;
then  t2 > (((1 - l) * w1) + (l * w2)) `2 by A5, A7, A8, A10, A19, XREAL_1:176;
hence  x in P by A1, A9, A17, A16; ::_thesis: verum
end;

theorem :: JORDAN21:6
for p being Point of (TOP-REAL 2) holds (north_halfline p) \ {p} is convex
proof
let p be Point of (TOP-REAL 2); ::_thesis: (north_halfline p) \ {p} is convex
set P = (north_halfline p) \ {p};
 (north_halfline p) \ {p} =  {  |[(p `1),r]| where r is Real : r > p `2  }
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  |[(p `1),r]| where r is Real : r > p `2  }  c= (north_halfline p) \ {p}
let x be set ; ::_thesis: ( x in (north_halfline p) \ {p} implies x in  {  |[(p `1),r]| where r is Real : r > p `2  }  )
assume A1: x in (north_halfline p) \ {p} ; ::_thesis: x in  {  |[(p `1),r]| where r is Real : r > p `2  }
then reconsider y = x as Point of (TOP-REAL 2) ;
A2: x in north_halfline p by A1, XBOOLE_0:def_5;
then A3: y `1 = p `1 by TOPREAL1:def_10;
then A4: x = |[(p `1),(y `2)]| by EUCLID:53;
A5: not x in {p} by A1, XBOOLE_0:def_5;
A6: now__::_thesis:_not_y_`2_=_p_`2
assume  y `2 = p `2 ; ::_thesis: contradiction
then  x = p by A3, TOPREAL3:6;
hence  contradiction by A5, TARSKI:def_1; ::_thesis: verum
end;
 y `2 >= p `2 by A2, TOPREAL1:def_10;
then  y `2 > p `2 by A6, XXREAL_0:1;
hence  x in  {  |[(p `1),r]| where r is Real : r > p `2  }  by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  |[(p `1),r]| where r is Real : r > p `2  }  or x in (north_halfline p) \ {p} )
assume  x in  {  |[(p `1),r]| where r is Real : r > p `2  }  ; ::_thesis: x in (north_halfline p) \ {p}
then consider r being Real such that
A7: x = |[(p `1),r]| and
A8: r > p `2 ;
reconsider y = x as Point of (TOP-REAL 2) by A7;
A9: y `2 = r by A7, EUCLID:52;
then A10: not x in {p} by A8, TARSKI:def_1;
 y `1 = p `1 by A7, EUCLID:52;
then  x in north_halfline p by A8, A9, TOPREAL1:def_10;
hence  x in (north_halfline p) \ {p} by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  (north_halfline p) \ {p} is convex by Th4; ::_thesis: verum
end;

theorem :: JORDAN21:7
for p being Point of (TOP-REAL 2) holds (south_halfline p) \ {p} is convex
proof
let p be Point of (TOP-REAL 2); ::_thesis: (south_halfline p) \ {p} is convex
set P = (south_halfline p) \ {p};
 (south_halfline p) \ {p} =  {  |[(p `1),r]| where r is Real : r < p `2  }
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  |[(p `1),r]| where r is Real : r < p `2  }  c= (south_halfline p) \ {p}
let x be set ; ::_thesis: ( x in (south_halfline p) \ {p} implies x in  {  |[(p `1),r]| where r is Real : r < p `2  }  )
assume A1: x in (south_halfline p) \ {p} ; ::_thesis: x in  {  |[(p `1),r]| where r is Real : r < p `2  }
then reconsider y = x as Point of (TOP-REAL 2) ;
A2: x in south_halfline p by A1, XBOOLE_0:def_5;
then A3: y `1 = p `1 by TOPREAL1:def_12;
then A4: x = |[(p `1),(y `2)]| by EUCLID:53;
A5: not x in {p} by A1, XBOOLE_0:def_5;
A6: now__::_thesis:_not_y_`2_=_p_`2
assume  y `2 = p `2 ; ::_thesis: contradiction
then  x = p by A3, TOPREAL3:6;
hence  contradiction by A5, TARSKI:def_1; ::_thesis: verum
end;
 y `2 <= p `2 by A2, TOPREAL1:def_12;
then  y `2 < p `2 by A6, XXREAL_0:1;
hence  x in  {  |[(p `1),r]| where r is Real : r < p `2  }  by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  |[(p `1),r]| where r is Real : r < p `2  }  or x in (south_halfline p) \ {p} )
assume  x in  {  |[(p `1),r]| where r is Real : r < p `2  }  ; ::_thesis: x in (south_halfline p) \ {p}
then consider r being Real such that
A7: x = |[(p `1),r]| and
A8: r < p `2 ;
reconsider y = x as Point of (TOP-REAL 2) by A7;
A9: y `2 = r by A7, EUCLID:52;
then A10: not x in {p} by A8, TARSKI:def_1;
 y `1 = p `1 by A7, EUCLID:52;
then  x in south_halfline p by A8, A9, TOPREAL1:def_12;
hence  x in (south_halfline p) \ {p} by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  (south_halfline p) \ {p} is convex by Th5; ::_thesis: verum
end;

theorem :: JORDAN21:8
for p being Point of (TOP-REAL 2) holds (west_halfline p) \ {p} is convex
proof
let p be Point of (TOP-REAL 2); ::_thesis: (west_halfline p) \ {p} is convex
set P = (west_halfline p) \ {p};
 (west_halfline p) \ {p} =  {  |[r,(p `2)]| where r is Real : r < p `1  }
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  |[r,(p `2)]| where r is Real : r < p `1  }  c= (west_halfline p) \ {p}
let x be set ; ::_thesis: ( x in (west_halfline p) \ {p} implies x in  {  |[r,(p `2)]| where r is Real : r < p `1  }  )
assume A1: x in (west_halfline p) \ {p} ; ::_thesis: x in  {  |[r,(p `2)]| where r is Real : r < p `1  }
then reconsider y = x as Point of (TOP-REAL 2) ;
A2: x in west_halfline p by A1, XBOOLE_0:def_5;
then A3: y `2 = p `2 by TOPREAL1:def_13;
then A4: x = |[(y `1),(p `2)]| by EUCLID:53;
A5: not x in {p} by A1, XBOOLE_0:def_5;
A6: now__::_thesis:_not_y_`1_=_p_`1
assume  y `1 = p `1 ; ::_thesis: contradiction
then  x = p by A3, TOPREAL3:6;
hence  contradiction by A5, TARSKI:def_1; ::_thesis: verum
end;
 y `1 <= p `1 by A2, TOPREAL1:def_13;
then  y `1 < p `1 by A6, XXREAL_0:1;
hence  x in  {  |[r,(p `2)]| where r is Real : r < p `1  }  by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  |[r,(p `2)]| where r is Real : r < p `1  }  or x in (west_halfline p) \ {p} )
assume  x in  {  |[r,(p `2)]| where r is Real : r < p `1  }  ; ::_thesis: x in (west_halfline p) \ {p}
then consider r being Real such that
A7: x = |[r,(p `2)]| and
A8: r < p `1 ;
reconsider y = x as Point of (TOP-REAL 2) by A7;
A9: y `1 = r by A7, EUCLID:52;
then A10: not x in {p} by A8, TARSKI:def_1;
 y `2 = p `2 by A7, EUCLID:52;
then  x in west_halfline p by A8, A9, TOPREAL1:def_13;
hence  x in (west_halfline p) \ {p} by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  (west_halfline p) \ {p} is convex by Th3; ::_thesis: verum
end;

theorem :: JORDAN21:9
for p being Point of (TOP-REAL 2) holds (east_halfline p) \ {p} is convex
proof
let p be Point of (TOP-REAL 2); ::_thesis: (east_halfline p) \ {p} is convex
set P = (east_halfline p) \ {p};
 (east_halfline p) \ {p} =  {  |[r,(p `2)]| where r is Real : r > p `1  }
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  |[r,(p `2)]| where r is Real : r > p `1  }  c= (east_halfline p) \ {p}
let x be set ; ::_thesis: ( x in (east_halfline p) \ {p} implies x in  {  |[r,(p `2)]| where r is Real : r > p `1  }  )
assume A1: x in (east_halfline p) \ {p} ; ::_thesis: x in  {  |[r,(p `2)]| where r is Real : r > p `1  }
then reconsider y = x as Point of (TOP-REAL 2) ;
A2: x in east_halfline p by A1, XBOOLE_0:def_5;
then A3: y `2 = p `2 by TOPREAL1:def_11;
then A4: x = |[(y `1),(p `2)]| by EUCLID:53;
A5: not x in {p} by A1, XBOOLE_0:def_5;
A6: now__::_thesis:_not_y_`1_=_p_`1
assume  y `1 = p `1 ; ::_thesis: contradiction
then  x = p by A3, TOPREAL3:6;
hence  contradiction by A5, TARSKI:def_1; ::_thesis: verum
end;
 y `1 >= p `1 by A2, TOPREAL1:def_11;
then  y `1 > p `1 by A6, XXREAL_0:1;
hence  x in  {  |[r,(p `2)]| where r is Real : r > p `1  }  by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  |[r,(p `2)]| where r is Real : r > p `1  }  or x in (east_halfline p) \ {p} )
assume  x in  {  |[r,(p `2)]| where r is Real : r > p `1  }  ; ::_thesis: x in (east_halfline p) \ {p}
then consider r being Real such that
A7: x = |[r,(p `2)]| and
A8: r > p `1 ;
reconsider y = x as Point of (TOP-REAL 2) by A7;
A9: y `1 = r by A7, EUCLID:52;
then A10: not x in {p} by A8, TARSKI:def_1;
 y `2 = p `2 by A7, EUCLID:52;
then  x in east_halfline p by A8, A9, TOPREAL1:def_11;
hence  x in (east_halfline p) \ {p} by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  (east_halfline p) \ {p} is convex by Th2; ::_thesis: verum
end;

theorem :: JORDAN21:10
for A being Subset of the carrier of (TOP-REAL 2) holds UBD A misses A
proof
let A be Subset of the carrier of (TOP-REAL 2); ::_thesis: UBD A misses A
 UBD A c= A ` by JORDAN2C:26;
hence  UBD A misses A by XBOOLE_1:63, XBOOLE_1:79; ::_thesis: verum
end;

theorem Th11: :: JORDAN21:11
for P being Subset of the carrier of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & p1 <> q1 & p2 <> q2 holds
( not p1 in Segment (P,p1,p2,q1,q2) & not p2 in Segment (P,p1,p2,q1,q2) )
proof
let P be Subset of the carrier of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & p1 <> q1 & p2 <> q2 holds
( not p1 in Segment (P,p1,p2,q1,q2) & not p2 in Segment (P,p1,p2,q1,q2) )
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & p1 <> q1 & p2 <> q2 implies ( not p1 in Segment (P,p1,p2,q1,q2) & not p2 in Segment (P,p1,p2,q1,q2) ) )
assume  ( P is_an_arc_of p1,p2 & p1 <> q1 & p2 <> q2 ) ; ::_thesis: ( not p1 in Segment (P,p1,p2,q1,q2) & not p2 in Segment (P,p1,p2,q1,q2) )
then A1: ( not p2 in L_Segment (P,p1,p2,q2) & not p1 in R_Segment (P,p1,p2,q1) ) by JORDAN6:59, JORDAN6:60;
 Segment (P,p1,p2,q1,q2) = (R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2)) by JORDAN6:def_5;
hence  ( not p1 in Segment (P,p1,p2,q1,q2) & not p2 in Segment (P,p1,p2,q1,q2) ) by A1, XBOOLE_0:def_4; ::_thesis: verum
end;

definition
let D be Subset of (TOP-REAL 2);
attrD is with_the_max_arc  means :Def1: :: JORDAN21:def 1
D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2);
end;

:: deftheorem Def1 defines with_the_max_arc JORDAN21:def_1_:_
 for D being Subset of (TOP-REAL 2) holds
( D is with_the_max_arc iff D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2) );

registration
cluster with_the_max_arc  ->  non empty for Element of K6( the carrier of (TOP-REAL 2));
coherence
 for b1 being Subset of (TOP-REAL 2) st b1 is with_the_max_arc holds
not b1 is empty
proof
let D be Subset of (TOP-REAL 2); ::_thesis: ( D is with_the_max_arc implies not D is empty )
assume  D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2) ; :: according to JORDAN21:def_1 ::_thesis: not D is empty
hence  not D is empty by XBOOLE_1:65; ::_thesis: verum
end;
end;

registration
cluster being_simple_closed_curve  ->  with_the_max_arc for Element of K6( the carrier of (TOP-REAL 2));
coherence
 for b1 being Simple_closed_curve holds b1 is with_the_max_arc
proof
let C be Simple_closed_curve; ::_thesis: C is with_the_max_arc
 (Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 by JORDAN6:65;
then  ( Upper_Middle_Point C in C & Upper_Middle_Point C in Vertical_Line (((W-bound C) + (E-bound C)) / 2) ) by JORDAN6:31, JORDAN6:68;
hence  C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by XBOOLE_0:3; :: according to JORDAN21:def_1 ::_thesis: verum
end;
end;

registration
cluster non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc for Element of K6( the carrier of (TOP-REAL 2));
existence
 not for b1 being Simple_closed_curve holds b1 is empty
proof
set A = the Simple_closed_curve;
take  the Simple_closed_curve ; ::_thesis: not the Simple_closed_curve is empty
thus  not the Simple_closed_curve is empty ; ::_thesis: verum
end;
end;

theorem Th12: :: JORDAN21:12
for D being with_the_max_arc Subset of (TOP-REAL 2) holds not proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is empty
proof
let D be with_the_max_arc Subset of (TOP-REAL 2); ::_thesis: not proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is empty
set w = ((W-bound D) + (E-bound D)) / 2;
 D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2) by Def1;
then  not D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) is empty by XBOOLE_0:def_7;
hence  not proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is empty by Lm1, RELAT_1:119; ::_thesis: verum
end;

theorem Th13: :: JORDAN21:13
for C being compact Subset of (TOP-REAL 2) holds
( proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is closed & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_below & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_above )
proof
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is closed & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_below & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_above )
set w = ((W-bound C) + (E-bound C)) / 2;
set X = C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2));
 Vertical_Line (((W-bound C) + (E-bound C)) / 2) is closed by JORDAN6:30;
then A1: C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed by TOPS_1:8;
 C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is bounded by RLTOPSP1:42, XBOOLE_1:17;
hence  proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is closed by A1, JCT_MISC:13; ::_thesis: ( proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_below & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_above )
 C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) c= C by XBOOLE_1:17;
then  proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is real-bounded by JCT_MISC:14, RLTOPSP1:42;
hence  ( proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_below & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_above ) by XXREAL_2:def_11; ::_thesis: verum
end;

begin

theorem Th14: :: JORDAN21:14
for C being Simple_closed_curve holds Lower_Middle_Point C in C
proof
let C be Simple_closed_curve; ::_thesis: Lower_Middle_Point C in C
 ( Lower_Middle_Point C in Lower_Arc C & Lower_Arc C c= C ) by JORDAN6:61, JORDAN6:66;
hence  Lower_Middle_Point C in C ; ::_thesis: verum
end;

theorem Th15: :: JORDAN21:15
for C being Simple_closed_curve holds (Lower_Middle_Point C) `2 <> (Upper_Middle_Point C) `2
proof
let C be Simple_closed_curve; ::_thesis: (Lower_Middle_Point C) `2 <> (Upper_Middle_Point C) `2
set l = Lower_Middle_Point C;
set u = Upper_Middle_Point C;
set w = ((W-bound C) + (E-bound C)) / 2;
A1: (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 by JORDAN6:64;
A2: (Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 by JORDAN6:65;
assume  (Lower_Middle_Point C) `2 = (Upper_Middle_Point C) `2 ; ::_thesis: contradiction
then  Lower_Middle_Point C = Upper_Middle_Point C by A1, A2, TOPREAL3:6;
then  ( Lower_Middle_Point C in Lower_Arc C & Lower_Middle_Point C in Upper_Arc C ) by JORDAN6:66, JORDAN6:67;
then  Lower_Middle_Point C in (Lower_Arc C) /\ (Upper_Arc C) by XBOOLE_0:def_4;
then  Lower_Middle_Point C in {(W-min C),(E-max C)} by JORDAN6:def_9;
then  ( Lower_Middle_Point C = W-min C or Lower_Middle_Point C = E-max C ) by TARSKI:def_2;
then  ( W-bound C = ((W-bound C) + (E-bound C)) / 2 or E-bound C = ((W-bound C) + (E-bound C)) / 2 ) by A1, EUCLID:52;
hence  contradiction by SPRECT_1:31; ::_thesis: verum
end;

theorem :: JORDAN21:16
for C being Simple_closed_curve holds Lower_Middle_Point C <> Upper_Middle_Point C
proof
let C be Simple_closed_curve; ::_thesis: Lower_Middle_Point C <> Upper_Middle_Point C
 (Lower_Middle_Point C) `2 <> (Upper_Middle_Point C) `2 by Th15;
hence  Lower_Middle_Point C <> Upper_Middle_Point C ; ::_thesis: verum
end;

begin

theorem Th17: :: JORDAN21:17
for C being Simple_closed_curve holds W-bound C = W-bound (Upper_Arc C)
proof
let C be Simple_closed_curve; ::_thesis: W-bound C = W-bound (Upper_Arc C)
A1: W-bound (Upper_Arc C) <= W-bound C
proof
A2: (W-min C) `1 = W-bound C by EUCLID:52;
assume A3: W-bound (Upper_Arc C) > W-bound C ; ::_thesis: contradiction
A4: west_halfline (W-min C) misses Upper_Arc C
proof
assume  west_halfline (W-min C) meets Upper_Arc C ; ::_thesis: contradiction
then consider p being set  such that
A5: p in west_halfline (W-min C) and
A6: p in Upper_Arc C by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A5;
 p `1 >= W-bound (Upper_Arc C) by A6, PSCOMP_1:24;
then  W-bound C < p `1 by A3, XXREAL_0:2;
hence  contradiction by A2, A5, TOPREAL1:def_13; ::_thesis: verum
end;
 ( W-min C in west_halfline (W-min C) & W-min C in Upper_Arc C ) by JORDAN7:1, TOPREAL1:38;
hence  contradiction by A4, XBOOLE_0:3; ::_thesis: verum
end;
 W-bound C <= W-bound (Upper_Arc C) by JORDAN6:61, PSCOMP_1:69;
hence  W-bound C = W-bound (Upper_Arc C) by A1, XXREAL_0:1; ::_thesis: verum
end;

theorem Th18: :: JORDAN21:18
for C being Simple_closed_curve holds E-bound C = E-bound (Upper_Arc C)
proof
let C be Simple_closed_curve; ::_thesis: E-bound C = E-bound (Upper_Arc C)
A1: E-bound (Upper_Arc C) >= E-bound C
proof
A2: (E-max C) `1 = E-bound C by EUCLID:52;
assume A3: E-bound (Upper_Arc C) < E-bound C ; ::_thesis: contradiction
A4: east_halfline (E-max C) misses Upper_Arc C
proof
assume  east_halfline (E-max C) meets Upper_Arc C ; ::_thesis: contradiction
then consider p being set  such that
A5: p in east_halfline (E-max C) and
A6: p in Upper_Arc C by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A5;
 p `1 <= E-bound (Upper_Arc C) by A6, PSCOMP_1:24;
then  E-bound C > p `1 by A3, XXREAL_0:2;
hence  contradiction by A2, A5, TOPREAL1:def_11; ::_thesis: verum
end;
 ( E-max C in east_halfline (E-max C) & E-max C in Upper_Arc C ) by JORDAN7:1, TOPREAL1:38;
hence  contradiction by A4, XBOOLE_0:3; ::_thesis: verum
end;
 E-bound C >= E-bound (Upper_Arc C) by JORDAN6:61, PSCOMP_1:67;
hence  E-bound C = E-bound (Upper_Arc C) by A1, XXREAL_0:1; ::_thesis: verum
end;

theorem Th19: :: JORDAN21:19
for C being Simple_closed_curve holds W-bound C = W-bound (Lower_Arc C)
proof
let C be Simple_closed_curve; ::_thesis: W-bound C = W-bound (Lower_Arc C)
A1: W-bound (Lower_Arc C) <= W-bound C
proof
A2: (W-min C) `1 = W-bound C by EUCLID:52;
assume A3: W-bound (Lower_Arc C) > W-bound C ; ::_thesis: contradiction
A4: west_halfline (W-min C) misses Lower_Arc C
proof
assume  west_halfline (W-min C) meets Lower_Arc C ; ::_thesis: contradiction
then consider p being set  such that
A5: p in west_halfline (W-min C) and
A6: p in Lower_Arc C by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A5;
 p `1 >= W-bound (Lower_Arc C) by A6, PSCOMP_1:24;
then  W-bound C < p `1 by A3, XXREAL_0:2;
hence  contradiction by A2, A5, TOPREAL1:def_13; ::_thesis: verum
end;
 ( W-min C in west_halfline (W-min C) & W-min C in Lower_Arc C ) by JORDAN7:1, TOPREAL1:38;
hence  contradiction by A4, XBOOLE_0:3; ::_thesis: verum
end;
 W-bound C <= W-bound (Lower_Arc C) by JORDAN6:61, PSCOMP_1:69;
hence  W-bound C = W-bound (Lower_Arc C) by A1, XXREAL_0:1; ::_thesis: verum
end;

theorem Th20: :: JORDAN21:20
for C being Simple_closed_curve holds E-bound C = E-bound (Lower_Arc C)
proof
let C be Simple_closed_curve; ::_thesis: E-bound C = E-bound (Lower_Arc C)
A1: E-bound (Lower_Arc C) >= E-bound C
proof
A2: (E-max C) `1 = E-bound C by EUCLID:52;
assume A3: E-bound (Lower_Arc C) < E-bound C ; ::_thesis: contradiction
A4: east_halfline (E-max C) misses Lower_Arc C
proof
assume  east_halfline (E-max C) meets Lower_Arc C ; ::_thesis: contradiction
then consider p being set  such that
A5: p in east_halfline (E-max C) and
A6: p in Lower_Arc C by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A5;
 p `1 <= E-bound (Lower_Arc C) by A6, PSCOMP_1:24;
then  E-bound C > p `1 by A3, XXREAL_0:2;
hence  contradiction by A2, A5, TOPREAL1:def_11; ::_thesis: verum
end;
 ( E-max C in east_halfline (E-max C) & E-max C in Lower_Arc C ) by JORDAN7:1, TOPREAL1:38;
hence  contradiction by A4, XBOOLE_0:3; ::_thesis: verum
end;
 E-bound C >= E-bound (Lower_Arc C) by JORDAN6:61, PSCOMP_1:67;
hence  E-bound C = E-bound (Lower_Arc C) by A1, XXREAL_0:1; ::_thesis: verum
end;

theorem Th21: :: JORDAN21:21
for C being Simple_closed_curve holds
( not (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )
proof
let C be Simple_closed_curve; ::_thesis: ( not (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )
set w = ((W-bound C) + (E-bound C)) / 2;
A1: W-bound C < E-bound C by SPRECT_1:31;
 (E-max C) `1 = E-bound C by EUCLID:52;
then A2: ((W-bound C) + (E-bound C)) / 2 <= (E-max C) `1 by A1, XREAL_1:226;
 (W-min C) `1 = W-bound C by EUCLID:52;
then  ( Upper_Arc C is_an_arc_of W-min C, E-max C & (W-min C) `1 <= ((W-bound C) + (E-bound C)) / 2 ) by A1, JORDAN6:def_8, XREAL_1:226;
then  Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A2, JORDAN6:49;
then  not (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty by XBOOLE_0:def_7;
hence  ( not (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty ) by Lm1, RELAT_1:119; ::_thesis: verum
end;

theorem Th22: :: JORDAN21:22
for C being Simple_closed_curve holds
( not (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )
proof
let C be Simple_closed_curve; ::_thesis: ( not (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )
set w = ((W-bound C) + (E-bound C)) / 2;
A1: W-bound C < E-bound C by SPRECT_1:31;
 (E-max C) `1 = E-bound C by EUCLID:52;
then A2: ((W-bound C) + (E-bound C)) / 2 <= (E-max C) `1 by A1, XREAL_1:226;
 Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:def_9;
then A3: Lower_Arc C is_an_arc_of W-min C, E-max C by JORDAN5B:14;
 (W-min C) `1 = W-bound C by EUCLID:52;
then  (W-min C) `1 <= ((W-bound C) + (E-bound C)) / 2 by A1, XREAL_1:226;
then  Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A3, A2, JORDAN6:49;
then  not (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty by XBOOLE_0:def_7;
hence  ( not (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty ) by Lm1, RELAT_1:119; ::_thesis: verum
end;

theorem :: JORDAN21:23
for C being Simple_closed_curve
for P being connected compact Subset of (TOP-REAL 2) st P c= C & W-min C in P & E-max C in P & not Upper_Arc C c= P holds
Lower_Arc C c= P
proof
let C be Simple_closed_curve; ::_thesis: for P being connected compact Subset of (TOP-REAL 2) st P c= C & W-min C in P & E-max C in P & not Upper_Arc C c= P holds
Lower_Arc C c= P
let P be connected compact Subset of (TOP-REAL 2); ::_thesis: ( P c= C & W-min C in P & E-max C in P & not Upper_Arc C c= P implies Lower_Arc C c= P )
assume that
A1: P c= C and
A2: W-min C in P and
A3: E-max C in P ; ::_thesis: ( Upper_Arc C c= P or Lower_Arc C c= P )
A4: now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_holds_not_P_=_{p}
given p being Point of (TOP-REAL 2) such that A5: P = {p} ; ::_thesis: contradiction
 ( W-min C = p & E-max C = p ) by A2, A3, A5, TARSKI:def_1;
hence  contradiction by TOPREAL5:19; ::_thesis: verum
end;
percases ( ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 or P = C ) by A1, A2, A4, BORSUK_4:56;
suppose ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 ; ::_thesis: ( Upper_Arc C c= P or Lower_Arc C c= P )
hence  ( Upper_Arc C c= P or Lower_Arc C c= P ) by A1, A2, A3, JORDAN16:22; ::_thesis: verum
end;
suppose P = C ; ::_thesis: ( Upper_Arc C c= P or Lower_Arc C c= P )
hence  ( Upper_Arc C c= P or Lower_Arc C c= P ) by JORDAN6:61; ::_thesis: verum
end;
end;
end;

registration
let C be Simple_closed_curve;
cluster Lower_Arc C ->  with_the_max_arc ;
coherence
 Lower_Arc C is with_the_max_arc
proof
 ( W-bound C = W-bound (Lower_Arc C) & E-bound C = E-bound (Lower_Arc C) ) by Th19, Th20;
hence  Lower_Arc C meets Vertical_Line (((W-bound (Lower_Arc C)) + (E-bound (Lower_Arc C))) / 2) by JORDAN6:62; :: according to JORDAN21:def_1 ::_thesis: verum
end;
cluster Upper_Arc C ->  with_the_max_arc ;
coherence
 Upper_Arc C is with_the_max_arc
proof
 ( W-bound C = W-bound (Upper_Arc C) & E-bound C = E-bound (Upper_Arc C) ) by Th17, Th18;
hence  Upper_Arc C meets Vertical_Line (((W-bound (Upper_Arc C)) + (E-bound (Upper_Arc C))) / 2) by JORDAN6:63; :: according to JORDAN21:def_1 ::_thesis: verum
end;
end;

begin

definition
let P be Subset of the carrier of (TOP-REAL 2);
func UMP P ->  Point of (TOP-REAL 2) equals :: JORDAN21:def 2
|[(((E-bound P) + (W-bound P)) / 2),(upper_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;
correctness
coherence
|[(((E-bound P) + (W-bound P)) / 2),(upper_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]| is Point of (TOP-REAL 2);
;
func LMP P ->  Point of (TOP-REAL 2) equals :: JORDAN21:def 3
|[(((E-bound P) + (W-bound P)) / 2),(lower_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;
correctness
coherence
|[(((E-bound P) + (W-bound P)) / 2),(lower_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]| is Point of (TOP-REAL 2);
;
end;

:: deftheorem  defines UMP JORDAN21:def_2_:_
 for P being Subset of the carrier of (TOP-REAL 2) holds UMP P = |[(((E-bound P) + (W-bound P)) / 2),(upper_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;

:: deftheorem  defines LMP JORDAN21:def_3_:_
 for P being Subset of the carrier of (TOP-REAL 2) holds LMP P = |[(((E-bound P) + (W-bound P)) / 2),(lower_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;

theorem Th24: :: JORDAN21:24
for C being compact non vertical Subset of (TOP-REAL 2) holds UMP C <> W-min C
proof
let C be compact non vertical Subset of (TOP-REAL 2); ::_thesis: UMP C <> W-min C
A1: ( (W-min C) `1 = W-bound C & (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 ) by EUCLID:52;
assume  UMP C = W-min C ; ::_thesis: contradiction
hence  contradiction by A1, SPRECT_1:31; ::_thesis: verum
end;

theorem Th25: :: JORDAN21:25
for C being compact non vertical Subset of (TOP-REAL 2) holds UMP C <> E-max C
proof
let C be compact non vertical Subset of (TOP-REAL 2); ::_thesis: UMP C <> E-max C
A1: ( (E-max C) `1 = E-bound C & (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 ) by EUCLID:52;
assume  UMP C = E-max C ; ::_thesis: contradiction
hence  contradiction by A1, SPRECT_1:31; ::_thesis: verum
end;

theorem Th26: :: JORDAN21:26
for C being compact non vertical Subset of (TOP-REAL 2) holds LMP C <> W-min C
proof
let C be compact non vertical Subset of (TOP-REAL 2); ::_thesis: LMP C <> W-min C
A1: ( (W-min C) `1 = W-bound C & (LMP C) `1 = ((W-bound C) + (E-bound C)) / 2 ) by EUCLID:52;
assume  LMP C = W-min C ; ::_thesis: contradiction
hence  contradiction by A1, SPRECT_1:31; ::_thesis: verum
end;

theorem Th27: :: JORDAN21:27
for C being compact non vertical Subset of (TOP-REAL 2) holds LMP C <> E-max C
proof
let C be compact non vertical Subset of (TOP-REAL 2); ::_thesis: LMP C <> E-max C
A1: ( (E-max C) `1 = E-bound C & (LMP C) `1 = ((W-bound C) + (E-bound C)) / 2 ) by EUCLID:52;
assume  LMP C = E-max C ; ::_thesis: contradiction
hence  contradiction by A1, SPRECT_1:31; ::_thesis: verum
end;

theorem :: JORDAN21:28
for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) holds
p `2 <= (UMP C) `2
proof
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) holds
p `2 <= (UMP C) `2
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) implies p `2 <= (UMP C) `2 )
assume A1: p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) ; ::_thesis: p `2 <= (UMP C) `2
 p `2 = proj2 . p by PSCOMP_1:def_6;
then A2: p `2 in proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A1, FUNCT_2:35;
 ( (UMP C) `2 = upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) & not proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above ) by A1, Lm1, Th13, EUCLID:52, RELAT_1:119;
hence  p `2 <= (UMP C) `2 by A2, SEQ_4:def_1; ::_thesis: verum
end;

theorem :: JORDAN21:29
for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) holds
(LMP C) `2 <= p `2
proof
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) holds
(LMP C) `2 <= p `2
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) implies (LMP C) `2 <= p `2 )
assume A1: p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) ; ::_thesis: (LMP C) `2 <= p `2
 p `2 = proj2 . p by PSCOMP_1:def_6;
then A2: p `2 in proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A1, FUNCT_2:35;
 ( (LMP C) `2 = lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) & not proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_below ) by A1, Lm1, Th13, EUCLID:52, RELAT_1:119;
hence  (LMP C) `2 <= p `2 by A2, SEQ_4:def_2; ::_thesis: verum
end;

theorem Th30: :: JORDAN21:30
for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds UMP D in D
proof
let D be compact with_the_max_arc Subset of (TOP-REAL 2); ::_thesis: UMP D in D
set w = ((W-bound D) + (E-bound D)) / 2;
set X = D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2));
 D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2) by Def1;
then A1: not D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) is empty by XBOOLE_0:def_7;
 ( proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is closed & proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is bounded_above ) by Th13;
then  upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) in proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) by A1, Lm1, RCOMP_1:12, RELAT_1:119;
then consider x being Point of (TOP-REAL 2) such that
A2: x in D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) and
A3: upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) = proj2 . x by Lm2;
 x in Vertical_Line (((W-bound D) + (E-bound D)) / 2) by A2, XBOOLE_0:def_4;
then A4: x `1 = ((W-bound D) + (E-bound D)) / 2 by JORDAN6:31
.= (UMP D) `1 by EUCLID:52 ;
x `2 = upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by A3, PSCOMP_1:def_6
.= (UMP D) `2 by EUCLID:52 ;
then  x = UMP D by A4, TOPREAL3:6;
hence  UMP D in D by A2, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th31: :: JORDAN21:31
for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds LMP D in D
proof
let D be compact with_the_max_arc Subset of (TOP-REAL 2); ::_thesis: LMP D in D
set w = ((W-bound D) + (E-bound D)) / 2;
set X = D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2));
A1: proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is bounded_below by Th13;
 ( not proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is empty & proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is closed ) by Th12, Th13;
then consider x being Point of (TOP-REAL 2) such that
A2: x in D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) and
A3: lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) = proj2 . x by A1, Lm2, RCOMP_1:13;
 x in Vertical_Line (((W-bound D) + (E-bound D)) / 2) by A2, XBOOLE_0:def_4;
then A4: x `1 = ((W-bound D) + (E-bound D)) / 2 by JORDAN6:31
.= (LMP D) `1 by EUCLID:52 ;
x `2 = lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by A3, PSCOMP_1:def_6
.= (LMP D) `2 by EUCLID:52 ;
then  x = LMP D by A4, TOPREAL3:6;
hence  LMP D in D by A2, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th32: :: JORDAN21:32
for P being Subset of (TOP-REAL 2) holds LSeg ((UMP P),|[(((W-bound P) + (E-bound P)) / 2),(N-bound P)]|) is vertical
proof
let P be Subset of (TOP-REAL 2); ::_thesis: LSeg ((UMP P),|[(((W-bound P) + (E-bound P)) / 2),(N-bound P)]|) is vertical
set w = ((W-bound P) + (E-bound P)) / 2;
 ( |[(((W-bound P) + (E-bound P)) / 2),(N-bound P)]| `1 = ((W-bound P) + (E-bound P)) / 2 & (UMP P) `1 = ((W-bound P) + (E-bound P)) / 2 ) by EUCLID:52;
hence  LSeg ((UMP P),|[(((W-bound P) + (E-bound P)) / 2),(N-bound P)]|) is vertical by SPPOL_1:16; ::_thesis: verum
end;

theorem Th33: :: JORDAN21:33
for P being Subset of (TOP-REAL 2) holds LSeg ((LMP P),|[(((W-bound P) + (E-bound P)) / 2),(S-bound P)]|) is vertical
proof
let P be Subset of (TOP-REAL 2); ::_thesis: LSeg ((LMP P),|[(((W-bound P) + (E-bound P)) / 2),(S-bound P)]|) is vertical
set w = ((W-bound P) + (E-bound P)) / 2;
 ( |[(((W-bound P) + (E-bound P)) / 2),(S-bound P)]| `1 = ((W-bound P) + (E-bound P)) / 2 & (LMP P) `1 = ((W-bound P) + (E-bound P)) / 2 ) by EUCLID:52;
hence  LSeg ((LMP P),|[(((W-bound P) + (E-bound P)) / 2),(S-bound P)]|) is vertical by SPPOL_1:16; ::_thesis: verum
end;

theorem Th34: :: JORDAN21:34
for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds (LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|)) /\ D = {(UMP D)}
proof
let D be compact with_the_max_arc Subset of (TOP-REAL 2); ::_thesis: (LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|)) /\ D = {(UMP D)}
set C = D;
set w = ((W-bound D) + (E-bound D)) / 2;
set L = LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|);
set X = D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2));
A1: UMP D in D by Th30;
A2: UMP D in LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) by RLTOPSP1:68;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(UMP D)} c= (LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|)) /\ D
let x be set ; ::_thesis: ( x in (LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|)) /\ D implies x in {(UMP D)} )
A3: (UMP D) `1 = ((W-bound D) + (E-bound D)) / 2 by EUCLID:52;
assume A4: x in (LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|)) /\ D ; ::_thesis: x in {(UMP D)}
then A5: x in LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) by XBOOLE_0:def_4;
reconsider y = x as Point of (TOP-REAL 2) by A4;
 UMP D in D by Th30;
then  ( |[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]| `2 = N-bound D & (UMP D) `2 <= N-bound D ) by EUCLID:52, PSCOMP_1:24;
then A6: (UMP D) `2 <= y `2 by A5, TOPREAL1:4;
A7: proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is bounded_above by Th13;
A8: (UMP D) `2 = upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by EUCLID:52;
A9: x in D by A4, XBOOLE_0:def_4;
 LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) is vertical by Th32;
then A10: y `1 = ((W-bound D) + (E-bound D)) / 2 by A2, A5, A3, SPPOL_1:def_3;
then  y in Vertical_Line (((W-bound D) + (E-bound D)) / 2) by JORDAN6:31;
then  ( y `2 = proj2 . y & y in D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) ) by A9, PSCOMP_1:def_6, XBOOLE_0:def_4;
then  y `2 in proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) by FUNCT_2:35;
then  y `2 <= upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by A7, SEQ_4:def_1;
then  y `2 = upper_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by A8, A6, XXREAL_0:1;
then  y = UMP D by A3, A8, A10, TOPREAL3:6;
hence  x in {(UMP D)} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(UMP D)} or x in (LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|)) /\ D )
assume  x in {(UMP D)} ; ::_thesis: x in (LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|)) /\ D
then  x = UMP D by TARSKI:def_1;
hence  x in (LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|)) /\ D by A2, A1, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th35: :: JORDAN21:35
for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D = {(LMP D)}
proof
let D be compact with_the_max_arc Subset of (TOP-REAL 2); ::_thesis: (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D = {(LMP D)}
set C = D;
set w = ((W-bound D) + (E-bound D)) / 2;
set L = LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|);
set X = D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2));
A1: LMP D in D by Th31;
A2: LMP D in LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) by RLTOPSP1:68;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(LMP D)} c= (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D
let x be set ; ::_thesis: ( x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D implies x in {(LMP D)} )
A3: (LMP D) `1 = ((W-bound D) + (E-bound D)) / 2 by EUCLID:52;
assume A4: x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D ; ::_thesis: x in {(LMP D)}
then A5: x in LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) by XBOOLE_0:def_4;
reconsider y = x as Point of (TOP-REAL 2) by A4;
 LMP D in D by Th31;
then  ( |[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]| `2 = S-bound D & (LMP D) `2 >= S-bound D ) by EUCLID:52, PSCOMP_1:24;
then A6: (LMP D) `2 >= y `2 by A5, TOPREAL1:4;
A7: proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is bounded_below by Th13;
A8: (LMP D) `2 = lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by EUCLID:52;
A9: x in D by A4, XBOOLE_0:def_4;
 LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) is vertical by Th33;
then A10: y `1 = ((W-bound D) + (E-bound D)) / 2 by A2, A5, A3, SPPOL_1:def_3;
then  y in Vertical_Line (((W-bound D) + (E-bound D)) / 2) by JORDAN6:31;
then  ( y `2 = proj2 . y & y in D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) ) by A9, PSCOMP_1:def_6, XBOOLE_0:def_4;
then  y `2 in proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) by FUNCT_2:35;
then  y `2 >= lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by A7, SEQ_4:def_2;
then  y `2 = lower_bound (proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)))) by A8, A6, XXREAL_0:1;
then  y = LMP D by A3, A8, A10, TOPREAL3:6;
hence  x in {(LMP D)} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(LMP D)} or x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D )
assume  x in {(LMP D)} ; ::_thesis: x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D
then  x = LMP D by TARSKI:def_1;
hence  x in (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D by A2, A1, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th36: :: JORDAN21:36
for C being Simple_closed_curve holds (LMP C) `2 < (UMP C) `2
proof
let C be Simple_closed_curve; ::_thesis: (LMP C) `2 < (UMP C) `2
set w = ((E-bound C) + (W-bound C)) / 2;
set X = C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2));
A1: ( (UMP C) `2 = upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) & (LMP C) `2 = lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) ) by EUCLID:52;
set u = Upper_Middle_Point C;
set l = Lower_Middle_Point C;
A2: (Lower_Middle_Point C) `2 = proj2 . (Lower_Middle_Point C) by PSCOMP_1:def_6;
 (Lower_Middle_Point C) `1 = ((E-bound C) + (W-bound C)) / 2 by JORDAN6:64;
then A3: Lower_Middle_Point C in Vertical_Line (((E-bound C) + (W-bound C)) / 2) by JORDAN6:31;
 Lower_Middle_Point C in C by Th14;
then  Lower_Middle_Point C in C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A3, XBOOLE_0:def_4;
then A4: (Lower_Middle_Point C) `2 in proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A2, FUNCT_2:35;
 C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is bounded by TOPREAL6:89;
then A5: proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is real-bounded by JCT_MISC:14;
 (Upper_Middle_Point C) `1 = ((E-bound C) + (W-bound C)) / 2 by JORDAN6:65;
then  ( Upper_Middle_Point C in C & Upper_Middle_Point C in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ) by JORDAN6:31, JORDAN6:68;
then A6: Upper_Middle_Point C in C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by XBOOLE_0:def_4;
 (Upper_Middle_Point C) `2 = proj2 . (Upper_Middle_Point C) by PSCOMP_1:def_6;
then A7: (Upper_Middle_Point C) `2 in proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A6, FUNCT_2:35;
 (Upper_Middle_Point C) `2 <> (Lower_Middle_Point C) `2 by Th15;
hence  (LMP C) `2 < (UMP C) `2 by A1, A5, A7, A4, SEQ_4:12; ::_thesis: verum
end;

theorem Th37: :: JORDAN21:37
for C being Simple_closed_curve holds UMP C <> LMP C
proof
let C be Simple_closed_curve; ::_thesis: UMP C <> LMP C
assume A1: UMP C = LMP C ; ::_thesis: contradiction
 (LMP C) `2 < (UMP C) `2 by Th36;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th38: :: JORDAN21:38
for C being Simple_closed_curve holds S-bound C < (UMP C) `2
proof
let C be Simple_closed_curve; ::_thesis: S-bound C < (UMP C) `2
set u = UMP C;
set l = LMP C;
A1: now__::_thesis:_not_S-bound_C_=_(UMP_C)_`2
assume A2: S-bound C = (UMP C) `2 ; ::_thesis: contradiction
 ( (LMP C) `2 < (UMP C) `2 & LMP C in C ) by Th31, Th36;
hence  contradiction by A2, PSCOMP_1:24; ::_thesis: verum
end;
 UMP C in C by Th30;
then  S-bound C <= (UMP C) `2 by PSCOMP_1:24;
hence  S-bound C < (UMP C) `2 by A1, XXREAL_0:1; ::_thesis: verum
end;

theorem Th39: :: JORDAN21:39
for C being Simple_closed_curve holds (UMP C) `2 <= N-bound C
proof
let C be Simple_closed_curve; ::_thesis: (UMP C) `2 <= N-bound C
 UMP C in C by Th30;
hence  (UMP C) `2 <= N-bound C by PSCOMP_1:24; ::_thesis: verum
end;

theorem Th40: :: JORDAN21:40
for C being Simple_closed_curve holds S-bound C <= (LMP C) `2
proof
let C be Simple_closed_curve; ::_thesis: S-bound C <= (LMP C) `2
 LMP C in C by Th31;
hence  S-bound C <= (LMP C) `2 by PSCOMP_1:24; ::_thesis: verum
end;

theorem Th41: :: JORDAN21:41
for C being Simple_closed_curve holds (LMP C) `2 < N-bound C
proof
let C be Simple_closed_curve; ::_thesis: (LMP C) `2 < N-bound C
set u = UMP C;
set l = LMP C;
A1: now__::_thesis:_not_N-bound_C_=_(LMP_C)_`2
assume A2: N-bound C = (LMP C) `2 ; ::_thesis: contradiction
 ( (LMP C) `2 < (UMP C) `2 & UMP C in C ) by Th30, Th36;
hence  contradiction by A2, PSCOMP_1:24; ::_thesis: verum
end;
 LMP C in C by Th31;
then  (LMP C) `2 <= N-bound C by PSCOMP_1:24;
hence  (LMP C) `2 < N-bound C by A1, XXREAL_0:1; ::_thesis: verum
end;

theorem Th42: :: JORDAN21:42
for C being Simple_closed_curve holds LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) misses LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)
proof
let C be Simple_closed_curve; ::_thesis: LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) misses LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)
set w = ((W-bound C) + (E-bound C)) / 2;
assume  LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) meets LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; ::_thesis: contradiction
then consider x being set  such that
A1: x in LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) and
A2: x in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A1;
 |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 = N-bound C by EUCLID:52;
then  (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by Th39;
then A3: x `2 >= (UMP C) `2 by A1, TOPREAL1:4;
 |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 = S-bound C by EUCLID:52;
then  |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (LMP C) `2 by Th40;
then  x `2 <= (LMP C) `2 by A2, TOPREAL1:4;
hence  contradiction by A3, Th36, XXREAL_0:2; ::_thesis: verum
end;

theorem :: JORDAN21:43
for A, B being Subset of (TOP-REAL 2) st A c= B & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_above holds
(UMP A) `2 <= (UMP B) `2
proof
let A, B be Subset of (TOP-REAL 2); ::_thesis: ( A c= B & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_above implies (UMP A) `2 <= (UMP B) `2 )
assume that
A1: A c= B and
A2: (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) and
A3: not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty and
A4: proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_above ; ::_thesis: (UMP A) `2 <= (UMP B) `2
set w = ((W-bound A) + (E-bound A)) / 2;
 ( not proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is empty & A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) c= B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) ) by A1, A3, Lm1, RELAT_1:119, XBOOLE_1:26;
then  upper_bound (proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) <= upper_bound (proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) by A4, RELAT_1:123, SEQ_4:48;
then  (UMP A) `2 <= upper_bound (proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) by EUCLID:52;
hence  (UMP A) `2 <= (UMP B) `2 by A2, EUCLID:52; ::_thesis: verum
end;

theorem :: JORDAN21:44
for A, B being Subset of (TOP-REAL 2) st A c= B & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_below holds
(LMP B) `2 <= (LMP A) `2
proof
let A, B be Subset of (TOP-REAL 2); ::_thesis: ( A c= B & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_below implies (LMP B) `2 <= (LMP A) `2 )
assume that
A1: A c= B and
A2: (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) and
A3: not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty and
A4: proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_below ; ::_thesis: (LMP B) `2 <= (LMP A) `2
set w = ((W-bound A) + (E-bound A)) / 2;
 ( not proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is empty & A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) c= B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) ) by A1, A3, Lm1, RELAT_1:119, XBOOLE_1:26;
then  lower_bound (proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) >= lower_bound (proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) by A4, RELAT_1:123, SEQ_4:47;
then  (LMP A) `2 >= lower_bound (proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) by EUCLID:52;
hence  (LMP B) `2 <= (LMP A) `2 by A2, EUCLID:52; ::_thesis: verum
end;

theorem :: JORDAN21:45
for A, B being Subset of (TOP-REAL 2) st A c= B & UMP B in A & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound B) + (E-bound B)) / 2))) is bounded_above & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) holds
UMP A = UMP B
proof
let A, B be Subset of (TOP-REAL 2); ::_thesis: ( A c= B & UMP B in A & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound B) + (E-bound B)) / 2))) is bounded_above & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) implies UMP A = UMP B )
assume that
A1: A c= B and
A2: UMP B in A and
A3: not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty and
A4: proj2 .: (B /\ (Vertical_Line (((W-bound B) + (E-bound B)) / 2))) is bounded_above and
A5: (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) ; ::_thesis: UMP A = UMP B
set w = ((W-bound A) + (E-bound A)) / 2;
A6: ( (UMP A) `2 = upper_bound (proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) & not proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is empty ) by A3, Lm1, EUCLID:52, RELAT_1:119;
A7: (UMP B) `1 = ((W-bound A) + (E-bound A)) / 2 by A5, EUCLID:52;
A8: for s being real number st 0 < s holds
ex r being real number st
( r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & ((UMP B) `2) - s < r )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & ((UMP B) `2) - s < r ) )
assume A9: 0 < s ; ::_thesis: ex r being real number st
( r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & ((UMP B) `2) - s < r )
take  (UMP B) `2 ; ::_thesis: ( (UMP B) `2 in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & ((UMP B) `2) - s < (UMP B) `2 )
 UMP B in Vertical_Line (((W-bound A) + (E-bound A)) / 2) by A7, JORDAN6:31;
then  ( proj2 . (UMP B) = (UMP B) `2 & UMP B in A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) ) by A2, PSCOMP_1:def_6, XBOOLE_0:def_4;
hence  (UMP B) `2 in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) by FUNCT_2:35; ::_thesis: ((UMP B) `2) - s < (UMP B) `2
 ((UMP B) `2) - s < ((UMP B) `2) - 0 by A9, XREAL_1:15;
hence  ((UMP B) `2) - s < (UMP B) `2 ; ::_thesis: verum
end;
A10: A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) c= B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) by A1, XBOOLE_1:26;
then A11: proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) c= proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) by RELAT_1:123;
 (UMP B) `2 = upper_bound (proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) by A5, EUCLID:52;
then A12: for r being real number st r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) holds
(UMP B) `2 >= r by A4, A5, A11, SEQ_4:def_1;
 proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_above by A4, A5, A10, RELAT_1:123, XXREAL_2:43;
then  ( (UMP A) `1 = ((W-bound A) + (E-bound A)) / 2 & (UMP A) `2 = (UMP B) `2 ) by A6, A12, A8, EUCLID:52, SEQ_4:def_1;
hence  UMP A = UMP B by A7, TOPREAL3:6; ::_thesis: verum
end;

theorem :: JORDAN21:46
for A, B being Subset of (TOP-REAL 2) st A c= B & LMP B in A & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound B) + (E-bound B)) / 2))) is bounded_below & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) holds
LMP A = LMP B
proof
let A, B be Subset of (TOP-REAL 2); ::_thesis: ( A c= B & LMP B in A & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound B) + (E-bound B)) / 2))) is bounded_below & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) implies LMP A = LMP B )
assume that
A1: A c= B and
A2: LMP B in A and
A3: not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty and
A4: proj2 .: (B /\ (Vertical_Line (((W-bound B) + (E-bound B)) / 2))) is bounded_below and
A5: (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) ; ::_thesis: LMP A = LMP B
set w = ((W-bound A) + (E-bound A)) / 2;
A6: ( (LMP A) `2 = lower_bound (proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) & not proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is empty ) by A3, Lm1, EUCLID:52, RELAT_1:119;
A7: (LMP B) `1 = ((W-bound A) + (E-bound A)) / 2 by A5, EUCLID:52;
A8: for s being real number st 0 < s holds
ex r being real number st
( r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & r < ((LMP B) `2) + s )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & r < ((LMP B) `2) + s ) )
assume A9: 0 < s ; ::_thesis: ex r being real number st
( r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & r < ((LMP B) `2) + s )
take  (LMP B) `2 ; ::_thesis: ( (LMP B) `2 in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) & (LMP B) `2 < ((LMP B) `2) + s )
 LMP B in Vertical_Line (((W-bound A) + (E-bound A)) / 2) by A7, JORDAN6:31;
then  ( proj2 . (LMP B) = (LMP B) `2 & LMP B in A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) ) by A2, PSCOMP_1:def_6, XBOOLE_0:def_4;
hence  (LMP B) `2 in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) by FUNCT_2:35; ::_thesis: (LMP B) `2 < ((LMP B) `2) + s
 ((LMP B) `2) + 0 < ((LMP B) `2) + s by A9, XREAL_1:6;
hence  (LMP B) `2 < ((LMP B) `2) + s ; ::_thesis: verum
end;
A10: A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) c= B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) by A1, XBOOLE_1:26;
then A11: proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) c= proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) by RELAT_1:123;
 (LMP B) `2 = lower_bound (proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)))) by A5, EUCLID:52;
then A12: for r being real number st r in proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) holds
(LMP B) `2 <= r by A4, A5, A11, SEQ_4:def_2;
 proj2 .: (A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_below by A4, A5, A10, RELAT_1:123, XXREAL_2:44;
then  ( (LMP A) `1 = ((W-bound A) + (E-bound A)) / 2 & (LMP A) `2 = (LMP B) `2 ) by A6, A12, A8, EUCLID:52, SEQ_4:def_2;
hence  LMP A = LMP B by A7, TOPREAL3:6; ::_thesis: verum
end;

theorem :: JORDAN21:47
for C being Simple_closed_curve holds (UMP (Upper_Arc C)) `2 <= N-bound C
proof
let C be Simple_closed_curve; ::_thesis: (UMP (Upper_Arc C)) `2 <= N-bound C
set w = ((E-bound C) + (W-bound C)) / 2;
A1: (Upper_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) c= C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by JORDAN6:61, XBOOLE_1:26;
 ( not proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above ) by Th13, Th21;
then A2: upper_bound (proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) <= upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by A1, RELAT_1:123, SEQ_4:48;
 ( W-bound C = W-bound (Upper_Arc C) & E-bound C = E-bound (Upper_Arc C) ) by Th17, Th18;
then A3: (UMP (Upper_Arc C)) `2 = upper_bound (proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52;
 ( (UMP C) `2 = upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) & (UMP C) `2 <= N-bound C ) by Th39, EUCLID:52;
hence  (UMP (Upper_Arc C)) `2 <= N-bound C by A2, A3, XXREAL_0:2; ::_thesis: verum
end;

theorem :: JORDAN21:48
for C being Simple_closed_curve holds S-bound C <= (LMP (Lower_Arc C)) `2
proof
let C be Simple_closed_curve; ::_thesis: S-bound C <= (LMP (Lower_Arc C)) `2
set w = ((E-bound C) + (W-bound C)) / 2;
A1: (Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) c= C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by JORDAN6:61, XBOOLE_1:26;
 ( not proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_below ) by Th13, Th22;
then A2: lower_bound (proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) >= lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by A1, RELAT_1:123, SEQ_4:47;
 ( W-bound C = W-bound (Lower_Arc C) & E-bound C = E-bound (Lower_Arc C) ) by Th19, Th20;
then A3: (LMP (Lower_Arc C)) `2 = lower_bound (proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52;
 ( (LMP C) `2 = lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) & S-bound C <= (LMP C) `2 ) by Th40, EUCLID:52;
hence  S-bound C <= (LMP (Lower_Arc C)) `2 by A2, A3, XXREAL_0:2; ::_thesis: verum
end;

theorem :: JORDAN21:49
for C being Simple_closed_curve holds
( not LMP C in Lower_Arc C or not UMP C in Lower_Arc C )
proof
let C be Simple_closed_curve; ::_thesis: ( not LMP C in Lower_Arc C or not UMP C in Lower_Arc C )
assume that
A1: LMP C in Lower_Arc C and
A2: UMP C in Lower_Arc C ; ::_thesis: contradiction
A3: (Upper_Arc C) /\ (Lower_Arc C) = {(W-min C),(E-max C)} by JORDAN6:def_9;
set n = |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|;
set S1 = LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C));
A4: Lower_Arc C c= C by JORDAN6:61;
A5: |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 = N-bound C by EUCLID:52;
set s = |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|;
set S2 = LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|);
A6: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:def_9;
A7: ( (W-min C) `1 = W-bound C & (E-max C) `1 = E-bound C ) by EUCLID:52;
A8: Upper_Arc C c= C by JORDAN6:61;
then A9: for p being Point of (TOP-REAL 2) st p in Upper_Arc C holds
( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A7, PSCOMP_1:24;
A10: UMP C <> E-max C by Th25;
A11: UMP C <> W-min C by Th24;
A12: now__::_thesis:_not_UMP_C_in_Upper_Arc_C
assume  UMP C in Upper_Arc C ; ::_thesis: contradiction
then  UMP C in (Upper_Arc C) /\ (Lower_Arc C) by A2, XBOOLE_0:def_4;
hence  contradiction by A11, A10, A3, TARSKI:def_2; ::_thesis: verum
end;
A13: W-bound C < E-bound C by SPRECT_1:31;
A14: Upper_Arc C misses LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))
proof
A15: (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ C = {(UMP C)} by Th34;
assume  Upper_Arc C meets LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) ; ::_thesis: contradiction
then consider x being set  such that
A16: x in Upper_Arc C and
A17: x in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) by XBOOLE_0:3;
 x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ C by A8, A16, A17, XBOOLE_0:def_4;
then A18: x = UMP C by A15, TARSKI:def_1;
then  x in (Lower_Arc C) /\ (Upper_Arc C) by A2, A16, XBOOLE_0:def_4;
hence  contradiction by A11, A10, A3, A18, TARSKI:def_2; ::_thesis: verum
end;
A19: ( UMP C in C & LMP C in C ) by Th30, Th31;
A20: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
 |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
then A21: LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) is vertical by A20, SPPOL_1:16;
A22: UMP C in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) by RLTOPSP1:68;
A23: LMP C <> E-max C by Th27;
A24: LMP C <> W-min C by Th26;
A25: now__::_thesis:_not_LMP_C_in_Upper_Arc_C
assume  LMP C in Upper_Arc C ; ::_thesis: contradiction
then  LMP C in (Upper_Arc C) /\ (Lower_Arc C) by A1, XBOOLE_0:def_4;
hence  contradiction by A24, A23, A3, TARSKI:def_2; ::_thesis: verum
end;
A26: LMP C <> UMP C by Th37;
A27: (LMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A28: Upper_Arc C misses LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)
proof
A29: (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C = {(LMP C)} by Th35;
assume  Upper_Arc C meets LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; ::_thesis: contradiction
then consider x being set  such that
A30: x in Upper_Arc C and
A31: x in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by XBOOLE_0:3;
 x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C by A8, A30, A31, XBOOLE_0:def_4;
then A32: x = LMP C by A29, TARSKI:def_1;
then  x in (Lower_Arc C) /\ (Upper_Arc C) by A1, A30, XBOOLE_0:def_4;
hence  contradiction by A24, A23, A3, A32, TARSKI:def_2; ::_thesis: verum
end;
 |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
then A33: LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is vertical by A27, SPPOL_1:16;
A34: LMP C in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by RLTOPSP1:68;
A35: LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) misses LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by Th42;
A36: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 = S-bound C by EUCLID:52;
then A37: ( Upper_Arc C is_an_arc_of W-min C, E-max C & ( for p being Point of (TOP-REAL 2) st p in Upper_Arc C holds
( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) ) ) by A8, A5, JORDAN6:def_8, PSCOMP_1:24;
percases ( LE LMP C, UMP C,C or LE UMP C, LMP C,C ) by A19, JORDAN16:7;
supposeA38: LE LMP C, UMP C,C ; ::_thesis: contradiction
set S = Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C));
A39: Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) c= Lower_Arc C by JORDAN16:2;
then A40: Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) c= C by A4, XBOOLE_1:1;
A41: now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_((LSeg_(|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_C)]|,(UMP_C)))_\/_(Segment_((Lower_Arc_C),(E-max_C),(W-min_C),(LMP_C),(UMP_C))))_\/_(LSeg_((LMP_C),|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_C)]|))_holds_
(_(W-min_C)_`1_<=_p_`1_&_p_`1_<=_(E-max_C)_`1_)
let p be Point of (TOP-REAL 2); ::_thesis: ( p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) implies ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 ) )
assume A42: p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
percases ( p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) or p in Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) or p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ) by A42, Lm3;
suppose p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
then  p `1 = (UMP C) `1 by A21, A22, SPPOL_1:def_3;
hence  ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A20, A7, A13, XREAL_1:226; ::_thesis: verum
end;
suppose p in Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
hence  ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A7, A40, PSCOMP_1:24; ::_thesis: verum
end;
suppose p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
then  p `1 = (LMP C) `1 by A33, A34, SPPOL_1:def_3;
hence  ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A27, A7, A13, XREAL_1:226; ::_thesis: verum
end;
end;
end;
A43: now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_((LSeg_(|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_C)]|,(UMP_C)))_\/_(Segment_((Lower_Arc_C),(E-max_C),(W-min_C),(LMP_C),(UMP_C))))_\/_(LSeg_((LMP_C),|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_C)]|))_holds_
(_|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_C)]|_`2_<=_p_`2_&_p_`2_<=_|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_C)]|_`2_)
let p be Point of (TOP-REAL 2); ::_thesis: ( p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) implies ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) )
assume A44: p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
percases ( p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) or p in Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) or p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ) by A44, Lm3;
supposeA45: p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
A46: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (UMP C) `2 by A36, Th38;
A47: (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A5, Th39;
then  (UMP C) `2 <= p `2 by A45, TOPREAL1:4;
hence  ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A45, A47, A46, TOPREAL1:4, XXREAL_0:2; ::_thesis: verum
end;
suppose p in Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
hence  ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A36, A5, A40, PSCOMP_1:24; ::_thesis: verum
end;
supposeA48: p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
A49: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (LMP C) `2 by A36, Th40;
hence  |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 by A48, TOPREAL1:4; ::_thesis: p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2
 p `2 <= (LMP C) `2 by A48, A49, TOPREAL1:4;
hence  p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A5, Th41, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A50: Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) c= (Lower_Arc C) \ {(W-min C),(E-max C)}
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) or s in (Lower_Arc C) \ {(W-min C),(E-max C)} )
assume A51: s in Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) ; ::_thesis: s in (Lower_Arc C) \ {(W-min C),(E-max C)}
now__::_thesis:_not_s_in_{(W-min_C),(E-max_C)}
assume  s in {(W-min C),(E-max C)} ; ::_thesis: contradiction
then  ( s = W-min C or s = E-max C ) by TARSKI:def_2;
hence  contradiction by A11, A23, A6, A51, Th11; ::_thesis: verum
end;
hence  s in (Lower_Arc C) \ {(W-min C),(E-max C)} by A39, A51, XBOOLE_0:def_5; ::_thesis: verum
end;
 Upper_Arc C misses Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))
proof
assume  Upper_Arc C meets Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) ; ::_thesis: contradiction
then consider x being set  such that
A52: x in Upper_Arc C and
A53: x in Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) by XBOOLE_0:3;
 x in Lower_Arc C by A50, A53, XBOOLE_0:def_5;
then  x in (Lower_Arc C) /\ (Upper_Arc C) by A52, XBOOLE_0:def_4;
hence  contradiction by A3, A50, A53, XBOOLE_0:def_5; ::_thesis: verum
end;
then A54: Upper_Arc C misses ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) by A14, A28, Lm4;
A55: LE LMP C, UMP C, Lower_Arc C, E-max C, W-min C by A25, A38, JORDAN6:def_10;
then A56: UMP C in Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) by JORDAN16:5;
A57: (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) = {(UMP C)}
proof
 (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ C = {(UMP C)} by Th34;
hence  (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) c= {(UMP C)} by A40, XBOOLE_1:26; :: according to XBOOLE_0:def_10 ::_thesis: {(UMP C)} c= (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(UMP C)} or x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) )
assume  x in {(UMP C)} ; ::_thesis: x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)))
then A58: x = UMP C by TARSKI:def_1;
 UMP C in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) by RLTOPSP1:68;
hence  x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) by A56, A58, XBOOLE_0:def_4; ::_thesis: verum
end;
A59: LMP C in Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) by A55, JORDAN16:5;
A60: (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) = {(LMP C)}
proof
 (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C = {(LMP C)} by Th35;
hence  (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) c= {(LMP C)} by A40, XBOOLE_1:26; :: according to XBOOLE_0:def_10 ::_thesis: {(LMP C)} c= (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(LMP C)} or x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) )
assume  x in {(LMP C)} ; ::_thesis: x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)))
then  x = LMP C by TARSKI:def_1;
hence  x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) by A34, A59, XBOOLE_0:def_4; ::_thesis: verum
end;
 Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) is_an_arc_of LMP C, UMP C by A26, A6, A55, JORDAN16:21;
then  Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)) is_an_arc_of UMP C, LMP C by JORDAN5B:14;
then A61: (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|, LMP C by A57, TOPREAL1:11;
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) = ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) \/ ((Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) by XBOOLE_1:23
.= {} \/ ((Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) by A35, XBOOLE_0:def_7 ;
then  ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| by A60, A61, TOPREAL1:10;
then  ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| by JORDAN5B:14;
hence  contradiction by A37, A9, A54, A43, A41, JGRAPH_1:44; ::_thesis: verum
end;
supposeA62: LE UMP C, LMP C,C ; ::_thesis: contradiction
set S = Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C));
A63: Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) c= Lower_Arc C by JORDAN16:2;
then A64: Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) c= C by A4, XBOOLE_1:1;
A65: now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_((LSeg_(|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_C)]|,(UMP_C)))_\/_(Segment_((Lower_Arc_C),(E-max_C),(W-min_C),(UMP_C),(LMP_C))))_\/_(LSeg_((LMP_C),|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_C)]|))_holds_
(_(W-min_C)_`1_<=_p_`1_&_p_`1_<=_(E-max_C)_`1_)
let p be Point of (TOP-REAL 2); ::_thesis: ( p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) implies ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 ) )
assume A66: p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
percases ( p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) or p in Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) or p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ) by A66, Lm3;
suppose p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
then  p `1 = (UMP C) `1 by A21, A22, SPPOL_1:def_3;
hence  ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A20, A7, A13, XREAL_1:226; ::_thesis: verum
end;
suppose p in Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
hence  ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A7, A64, PSCOMP_1:24; ::_thesis: verum
end;
suppose p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
then  p `1 = (LMP C) `1 by A33, A34, SPPOL_1:def_3;
hence  ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A27, A7, A13, XREAL_1:226; ::_thesis: verum
end;
end;
end;
A67: now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_((LSeg_(|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_C)]|,(UMP_C)))_\/_(Segment_((Lower_Arc_C),(E-max_C),(W-min_C),(UMP_C),(LMP_C))))_\/_(LSeg_((LMP_C),|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_C)]|))_holds_
(_|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_C)]|_`2_<=_p_`2_&_p_`2_<=_|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_C)]|_`2_)
let p be Point of (TOP-REAL 2); ::_thesis: ( p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) implies ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) )
assume A68: p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
percases ( p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) or p in Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) or p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ) by A68, Lm3;
supposeA69: p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
A70: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (UMP C) `2 by A36, Th38;
A71: (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A5, Th39;
then  (UMP C) `2 <= p `2 by A69, TOPREAL1:4;
hence  ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A69, A71, A70, TOPREAL1:4, XXREAL_0:2; ::_thesis: verum
end;
suppose p in Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
hence  ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A36, A5, A64, PSCOMP_1:24; ::_thesis: verum
end;
supposeA72: p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
A73: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (LMP C) `2 by A36, Th40;
hence  |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 by A72, TOPREAL1:4; ::_thesis: p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2
 p `2 <= (LMP C) `2 by A72, A73, TOPREAL1:4;
hence  p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A5, Th41, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A74: Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) c= (Lower_Arc C) \ {(W-min C),(E-max C)}
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) or s in (Lower_Arc C) \ {(W-min C),(E-max C)} )
assume A75: s in Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) ; ::_thesis: s in (Lower_Arc C) \ {(W-min C),(E-max C)}
now__::_thesis:_not_s_in_{(W-min_C),(E-max_C)}
assume  s in {(W-min C),(E-max C)} ; ::_thesis: contradiction
then  ( s = W-min C or s = E-max C ) by TARSKI:def_2;
hence  contradiction by A10, A24, A6, A75, Th11; ::_thesis: verum
end;
hence  s in (Lower_Arc C) \ {(W-min C),(E-max C)} by A63, A75, XBOOLE_0:def_5; ::_thesis: verum
end;
 Upper_Arc C misses Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))
proof
assume  Upper_Arc C meets Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) ; ::_thesis: contradiction
then consider x being set  such that
A76: x in Upper_Arc C and
A77: x in Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) by XBOOLE_0:3;
 x in Lower_Arc C by A74, A77, XBOOLE_0:def_5;
then  x in (Lower_Arc C) /\ (Upper_Arc C) by A76, XBOOLE_0:def_4;
hence  contradiction by A3, A74, A77, XBOOLE_0:def_5; ::_thesis: verum
end;
then A78: Upper_Arc C misses ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) by A14, A28, Lm4;
A79: LE UMP C, LMP C, Lower_Arc C, E-max C, W-min C by A12, A62, JORDAN6:def_10;
then A80: UMP C in Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) by JORDAN16:5;
A81: (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) = {(UMP C)}
proof
 (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ C = {(UMP C)} by Th34;
hence  (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) c= {(UMP C)} by A64, XBOOLE_1:26; :: according to XBOOLE_0:def_10 ::_thesis: {(UMP C)} c= (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(UMP C)} or x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) )
assume  x in {(UMP C)} ; ::_thesis: x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)))
then A82: x = UMP C by TARSKI:def_1;
 UMP C in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) by RLTOPSP1:68;
hence  x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) by A80, A82, XBOOLE_0:def_4; ::_thesis: verum
end;
A83: LMP C in Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) by A79, JORDAN16:5;
A84: (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) = {(LMP C)}
proof
 (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C = {(LMP C)} by Th35;
hence  (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) c= {(LMP C)} by A64, XBOOLE_1:26; :: according to XBOOLE_0:def_10 ::_thesis: {(LMP C)} c= (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(LMP C)} or x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) )
assume  x in {(LMP C)} ; ::_thesis: x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)))
then  x = LMP C by TARSKI:def_1;
hence  x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) by A34, A83, XBOOLE_0:def_4; ::_thesis: verum
end;
 Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)) is_an_arc_of UMP C, LMP C by A6, A79, Th37, JORDAN16:21;
then A85: (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|, LMP C by A81, TOPREAL1:11;
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) = ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) \/ ((Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) by XBOOLE_1:23
.= {} \/ ((Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) by A35, XBOOLE_0:def_7 ;
then  ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| by A84, A85, TOPREAL1:10;
then  ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Lower_Arc C),(E-max C),(W-min C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| by JORDAN5B:14;
hence  contradiction by A37, A9, A78, A67, A65, JGRAPH_1:44; ::_thesis: verum
end;
end;
end;

theorem :: JORDAN21:50
for C being Simple_closed_curve holds
( not LMP C in Upper_Arc C or not UMP C in Upper_Arc C )
proof
let C be Simple_closed_curve; ::_thesis: ( not LMP C in Upper_Arc C or not UMP C in Upper_Arc C )
assume that
A1: LMP C in Upper_Arc C and
A2: UMP C in Upper_Arc C ; ::_thesis: contradiction
A3: (Upper_Arc C) /\ (Lower_Arc C) = {(W-min C),(E-max C)} by JORDAN6:def_9;
set s = |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|;
set S2 = LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|);
A4: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:def_8;
 Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:def_9;
then A5: Lower_Arc C is_an_arc_of W-min C, E-max C by JORDAN5B:14;
A6: ( UMP C in C & LMP C in C ) by Th30, Th31;
A7: (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
set n = |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|;
set S1 = LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C));
A8: Upper_Arc C c= C by JORDAN6:61;
A9: |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 = N-bound C by EUCLID:52;
 |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
then A10: LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) is vertical by A7, SPPOL_1:16;
A11: LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) misses LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by Th42;
A12: UMP C in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) by RLTOPSP1:68;
A13: ( (W-min C) `1 = W-bound C & (E-max C) `1 = E-bound C ) by EUCLID:52;
A14: Lower_Arc C c= C by JORDAN6:61;
then A15: for p being Point of (TOP-REAL 2) st p in Lower_Arc C holds
( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A13, PSCOMP_1:24;
A16: UMP C <> E-max C by Th25;
A17: UMP C <> W-min C by Th24;
A18: now__::_thesis:_not_UMP_C_in_Lower_Arc_C
assume  UMP C in Lower_Arc C ; ::_thesis: contradiction
then  UMP C in (Upper_Arc C) /\ (Lower_Arc C) by A2, XBOOLE_0:def_4;
hence  contradiction by A17, A16, A3, TARSKI:def_2; ::_thesis: verum
end;
A19: W-bound C < E-bound C by SPRECT_1:31;
A20: Lower_Arc C misses LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))
proof
A21: (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ C = {(UMP C)} by Th34;
assume  Lower_Arc C meets LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) ; ::_thesis: contradiction
then consider x being set  such that
A22: x in Lower_Arc C and
A23: x in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) by XBOOLE_0:3;
 x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ C by A14, A22, A23, XBOOLE_0:def_4;
then A24: x = UMP C by A21, TARSKI:def_1;
then  x in (Lower_Arc C) /\ (Upper_Arc C) by A2, A22, XBOOLE_0:def_4;
hence  contradiction by A17, A16, A3, A24, TARSKI:def_2; ::_thesis: verum
end;
A25: LMP C <> E-max C by Th27;
A26: LMP C <> W-min C by Th26;
A27: now__::_thesis:_not_LMP_C_in_Lower_Arc_C
assume  LMP C in Lower_Arc C ; ::_thesis: contradiction
then  LMP C in (Upper_Arc C) /\ (Lower_Arc C) by A1, XBOOLE_0:def_4;
hence  contradiction by A26, A25, A3, TARSKI:def_2; ::_thesis: verum
end;
A28: LMP C <> UMP C by Th37;
A29: (LMP C) `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
A30: Lower_Arc C misses LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)
proof
A31: (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C = {(LMP C)} by Th35;
assume  Lower_Arc C meets LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; ::_thesis: contradiction
then consider x being set  such that
A32: x in Lower_Arc C and
A33: x in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by XBOOLE_0:3;
 x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C by A14, A32, A33, XBOOLE_0:def_4;
then A34: x = LMP C by A31, TARSKI:def_1;
then  x in (Lower_Arc C) /\ (Upper_Arc C) by A1, A32, XBOOLE_0:def_4;
hence  contradiction by A26, A25, A3, A34, TARSKI:def_2; ::_thesis: verum
end;
 |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `1 = ((W-bound C) + (E-bound C)) / 2 by EUCLID:52;
then A35: LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) is vertical by A29, SPPOL_1:16;
A36: LMP C in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) by RLTOPSP1:68;
A37: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 = S-bound C by EUCLID:52;
then A38: for p being Point of (TOP-REAL 2) st p in Lower_Arc C holds
( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A14, A9, PSCOMP_1:24;
percases ( LE LMP C, UMP C,C or LE UMP C, LMP C,C ) by A6, JORDAN16:7;
supposeA39: LE LMP C, UMP C,C ; ::_thesis: contradiction
set S = Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C));
A40: Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) c= Upper_Arc C by JORDAN16:2;
then A41: Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) c= C by A8, XBOOLE_1:1;
A42: now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_((LSeg_(|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_C)]|,(UMP_C)))_\/_(Segment_((Upper_Arc_C),(W-min_C),(E-max_C),(LMP_C),(UMP_C))))_\/_(LSeg_((LMP_C),|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_C)]|))_holds_
(_(W-min_C)_`1_<=_p_`1_&_p_`1_<=_(E-max_C)_`1_)
let p be Point of (TOP-REAL 2); ::_thesis: ( p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) implies ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 ) )
assume A43: p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
percases ( p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) or p in Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) or p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ) by A43, Lm3;
suppose p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
then  p `1 = (UMP C) `1 by A10, A12, SPPOL_1:def_3;
hence  ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A7, A13, A19, XREAL_1:226; ::_thesis: verum
end;
suppose p in Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
hence  ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A13, A41, PSCOMP_1:24; ::_thesis: verum
end;
suppose p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
then  p `1 = (LMP C) `1 by A35, A36, SPPOL_1:def_3;
hence  ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A29, A13, A19, XREAL_1:226; ::_thesis: verum
end;
end;
end;
A44: now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_((LSeg_(|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_C)]|,(UMP_C)))_\/_(Segment_((Upper_Arc_C),(W-min_C),(E-max_C),(LMP_C),(UMP_C))))_\/_(LSeg_((LMP_C),|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_C)]|))_holds_
(_|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_C)]|_`2_<=_p_`2_&_p_`2_<=_|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_C)]|_`2_)
let p be Point of (TOP-REAL 2); ::_thesis: ( p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) implies ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) )
assume A45: p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
percases ( p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) or p in Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) or p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ) by A45, Lm3;
supposeA46: p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
A47: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (UMP C) `2 by A37, Th38;
A48: (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A9, Th39;
then  (UMP C) `2 <= p `2 by A46, TOPREAL1:4;
hence  ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A46, A48, A47, TOPREAL1:4, XXREAL_0:2; ::_thesis: verum
end;
suppose p in Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
hence  ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A37, A9, A41, PSCOMP_1:24; ::_thesis: verum
end;
supposeA49: p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
A50: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (LMP C) `2 by A37, Th40;
hence  |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 by A49, TOPREAL1:4; ::_thesis: p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2
 p `2 <= (LMP C) `2 by A49, A50, TOPREAL1:4;
hence  p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A9, Th41, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A51: Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) c= (Upper_Arc C) \ {(W-min C),(E-max C)}
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) or s in (Upper_Arc C) \ {(W-min C),(E-max C)} )
assume A52: s in Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) ; ::_thesis: s in (Upper_Arc C) \ {(W-min C),(E-max C)}
now__::_thesis:_not_s_in_{(W-min_C),(E-max_C)}
assume  s in {(W-min C),(E-max C)} ; ::_thesis: contradiction
then  ( s = W-min C or s = E-max C ) by TARSKI:def_2;
hence  contradiction by A16, A26, A4, A52, Th11; ::_thesis: verum
end;
hence  s in (Upper_Arc C) \ {(W-min C),(E-max C)} by A40, A52, XBOOLE_0:def_5; ::_thesis: verum
end;
 Lower_Arc C misses Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C))
proof
assume  Lower_Arc C meets Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) ; ::_thesis: contradiction
then consider x being set  such that
A53: x in Lower_Arc C and
A54: x in Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) by XBOOLE_0:3;
 x in Upper_Arc C by A51, A54, XBOOLE_0:def_5;
then  x in (Lower_Arc C) /\ (Upper_Arc C) by A53, XBOOLE_0:def_4;
hence  contradiction by A3, A51, A54, XBOOLE_0:def_5; ::_thesis: verum
end;
then A55: Lower_Arc C misses ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) by A20, A30, Lm4;
A56: LE LMP C, UMP C, Upper_Arc C, W-min C, E-max C by A18, A39, JORDAN6:def_10;
then A57: UMP C in Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) by JORDAN16:5;
A58: (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C))) = {(UMP C)}
proof
 (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ C = {(UMP C)} by Th34;
hence  (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C))) c= {(UMP C)} by A41, XBOOLE_1:26; :: according to XBOOLE_0:def_10 ::_thesis: {(UMP C)} c= (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(UMP C)} or x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C))) )
assume  x in {(UMP C)} ; ::_thesis: x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)))
then A59: x = UMP C by TARSKI:def_1;
 UMP C in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) by RLTOPSP1:68;
hence  x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C))) by A57, A59, XBOOLE_0:def_4; ::_thesis: verum
end;
A60: LMP C in Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) by A56, JORDAN16:5;
A61: (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C))) = {(LMP C)}
proof
 (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C = {(LMP C)} by Th35;
hence  (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C))) c= {(LMP C)} by A41, XBOOLE_1:26; :: according to XBOOLE_0:def_10 ::_thesis: {(LMP C)} c= (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(LMP C)} or x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C))) )
assume  x in {(LMP C)} ; ::_thesis: x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)))
then  x = LMP C by TARSKI:def_1;
hence  x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C))) by A36, A60, XBOOLE_0:def_4; ::_thesis: verum
end;
 Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) is_an_arc_of LMP C, UMP C by A28, A4, A56, JORDAN16:21;
then  Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)) is_an_arc_of UMP C, LMP C by JORDAN5B:14;
then A62: (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C))) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|, LMP C by A58, TOPREAL1:11;
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) = ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) \/ ((Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) by XBOOLE_1:23
.= {} \/ ((Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) by A11, XBOOLE_0:def_7 ;
then  ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| by A61, A62, TOPREAL1:10;
then  ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(LMP C),(UMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| by JORDAN5B:14;
hence  contradiction by A5, A38, A15, A55, A44, A42, JGRAPH_1:44; ::_thesis: verum
end;
supposeA63: LE UMP C, LMP C,C ; ::_thesis: contradiction
set S = Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C));
A64: Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) c= Upper_Arc C by JORDAN16:2;
then A65: Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) c= C by A8, XBOOLE_1:1;
A66: now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_((LSeg_(|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_C)]|,(UMP_C)))_\/_(Segment_((Upper_Arc_C),(W-min_C),(E-max_C),(UMP_C),(LMP_C))))_\/_(LSeg_((LMP_C),|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_C)]|))_holds_
(_(W-min_C)_`1_<=_p_`1_&_p_`1_<=_(E-max_C)_`1_)
let p be Point of (TOP-REAL 2); ::_thesis: ( p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) implies ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 ) )
assume A67: p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
percases ( p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) or p in Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) or p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ) by A67, Lm3;
suppose p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
then  p `1 = (UMP C) `1 by A10, A12, SPPOL_1:def_3;
hence  ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A7, A13, A19, XREAL_1:226; ::_thesis: verum
end;
suppose p in Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
hence  ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A13, A65, PSCOMP_1:24; ::_thesis: verum
end;
suppose p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; ::_thesis: ( (W-min C) `1 <= b1 `1 & b1 `1 <= (E-max C) `1 )
then  p `1 = (LMP C) `1 by A35, A36, SPPOL_1:def_3;
hence  ( (W-min C) `1 <= p `1 & p `1 <= (E-max C) `1 ) by A29, A13, A19, XREAL_1:226; ::_thesis: verum
end;
end;
end;
A68: now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_st_p_in_((LSeg_(|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_C)]|,(UMP_C)))_\/_(Segment_((Upper_Arc_C),(W-min_C),(E-max_C),(UMP_C),(LMP_C))))_\/_(LSeg_((LMP_C),|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_C)]|))_holds_
(_|[(((W-bound_C)_+_(E-bound_C))_/_2),(S-bound_C)]|_`2_<=_p_`2_&_p_`2_<=_|[(((W-bound_C)_+_(E-bound_C))_/_2),(N-bound_C)]|_`2_)
let p be Point of (TOP-REAL 2); ::_thesis: ( p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) implies ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) )
assume A69: p in ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
percases ( p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) or p in Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) or p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ) by A69, Lm3;
supposeA70: p in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
A71: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (UMP C) `2 by A37, Th38;
A72: (UMP C) `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A9, Th39;
then  (UMP C) `2 <= p `2 by A70, TOPREAL1:4;
hence  ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A70, A72, A71, TOPREAL1:4, XXREAL_0:2; ::_thesis: verum
end;
suppose p in Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
hence  ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 & p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 ) by A37, A9, A65, PSCOMP_1:24; ::_thesis: verum
end;
supposeA73: p in LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|) ; ::_thesis: ( |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= b1 `2 & b1 `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 )
A74: |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= (LMP C) `2 by A37, Th40;
hence  |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| `2 <= p `2 by A73, TOPREAL1:4; ::_thesis: p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2
 p `2 <= (LMP C) `2 by A73, A74, TOPREAL1:4;
hence  p `2 <= |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| `2 by A9, Th41, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A75: Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) c= (Upper_Arc C) \ {(W-min C),(E-max C)}
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) or s in (Upper_Arc C) \ {(W-min C),(E-max C)} )
assume A76: s in Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) ; ::_thesis: s in (Upper_Arc C) \ {(W-min C),(E-max C)}
now__::_thesis:_not_s_in_{(W-min_C),(E-max_C)}
assume  s in {(W-min C),(E-max C)} ; ::_thesis: contradiction
then  ( s = W-min C or s = E-max C ) by TARSKI:def_2;
hence  contradiction by A17, A25, A4, A76, Th11; ::_thesis: verum
end;
hence  s in (Upper_Arc C) \ {(W-min C),(E-max C)} by A64, A76, XBOOLE_0:def_5; ::_thesis: verum
end;
 Lower_Arc C misses Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C))
proof
assume  Lower_Arc C meets Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) ; ::_thesis: contradiction
then consider x being set  such that
A77: x in Lower_Arc C and
A78: x in Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) by XBOOLE_0:3;
 x in Upper_Arc C by A75, A78, XBOOLE_0:def_5;
then  x in (Lower_Arc C) /\ (Upper_Arc C) by A77, XBOOLE_0:def_4;
hence  contradiction by A3, A75, A78, XBOOLE_0:def_5; ::_thesis: verum
end;
then A79: Lower_Arc C misses ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) by A20, A30, Lm4;
A80: LE UMP C, LMP C, Upper_Arc C, W-min C, E-max C by A27, A63, JORDAN6:def_10;
then A81: UMP C in Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) by JORDAN16:5;
A82: (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C))) = {(UMP C)}
proof
 (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ C = {(UMP C)} by Th34;
hence  (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C))) c= {(UMP C)} by A65, XBOOLE_1:26; :: according to XBOOLE_0:def_10 ::_thesis: {(UMP C)} c= (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(UMP C)} or x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C))) )
assume  x in {(UMP C)} ; ::_thesis: x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)))
then A83: x = UMP C by TARSKI:def_1;
 UMP C in LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C)) by RLTOPSP1:68;
hence  x in (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C))) by A81, A83, XBOOLE_0:def_4; ::_thesis: verum
end;
A84: LMP C in Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) by A80, JORDAN16:5;
A85: (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C))) = {(LMP C)}
proof
 (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ C = {(LMP C)} by Th35;
hence  (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C))) c= {(LMP C)} by A65, XBOOLE_1:26; :: according to XBOOLE_0:def_10 ::_thesis: {(LMP C)} c= (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(LMP C)} or x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C))) )
assume  x in {(LMP C)} ; ::_thesis: x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)))
then  x = LMP C by TARSKI:def_1;
hence  x in (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) /\ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C))) by A36, A84, XBOOLE_0:def_4; ::_thesis: verum
end;
 Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)) is_an_arc_of UMP C, LMP C by A4, A80, Th37, JORDAN16:21;
then A86: (LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C))) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|, LMP C by A82, TOPREAL1:11;
((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) = ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) \/ ((Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) by XBOOLE_1:23
.= {} \/ ((Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C))) /\ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|))) by A11, XBOOLE_0:def_7 ;
then  ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]| by A85, A86, TOPREAL1:10;
then  ((LSeg (|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|,(UMP C))) \/ (Segment ((Upper_Arc C),(W-min C),(E-max C),(UMP C),(LMP C)))) \/ (LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)) is_an_arc_of |[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|,|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| by JORDAN5B:14;
hence  contradiction by A5, A38, A15, A79, A68, A66, JGRAPH_1:44; ::_thesis: verum
end;
end;
end;