reconsider h2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
reconsider Q = Vertical_Line 0 as Subset of (TOP-REAL 2) ;
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } implies Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } )
set P4 = Lower_Arc P;
reconsider P1 = Lower_Arc P as Subset of (TOP-REAL 2) ;
reconsider P2 = Upper_Arc P as Subset of (TOP-REAL 2) ;
set pj = First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0));
set p8 = Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0));
A1: LSeg (|[0,(- 1)]|,|[0,1]|) c= Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg (|[0,(- 1)]|,|[0,1]|) or x in Q )
assume x in LSeg (|[0,(- 1)]|,|[0,1]|) ; :: thesis: x in Q
then consider l being Real such that
A2: x = ((1 - l) * |[0,(- 1)]|) + (l * |[0,1]|) and
0 <= l and
l <= 1 ;
(((1 - l) * |[0,(- 1)]|) + (l * |[0,1]|)) `1 = (((1 - l) * |[0,(- 1)]|) `1) + ((l * |[0,1]|) `1) by TOPREAL3:2
.= ((1 - l) * (|[0,(- 1)]| `1)) + ((l * |[0,1]|) `1) by TOPREAL3:4
.= ((1 - l) * (|[0,(- 1)]| `1)) + (l * (|[0,1]| `1)) by TOPREAL3:4
.= ((1 - l) * 0) + (l * (|[0,1]| `1)) by EUCLID:52
.= ((1 - l) * 0) + (l * 0) by EUCLID:52
.= 0 ;
hence x in Q by A2; :: thesis: verum

end;

assume A3: P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } ; :: thesis: Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) }
then A4: P is being_simple_closed_curve by JGRAPH_3:26;
then A5: (Upper_Arc P) \/ (Lower_Arc P) = P by JORDAN6:def 9;
then A6: Lower_Arc P c= P by XBOOLE_1:7;
A7: P2 /\ Q c= {|[0,(- 1)]|,|[0,1]|}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P2 /\ Q or x in {|[0,(- 1)]|,|[0,1]|} )
assume A8: x in P2 /\ Q ; :: thesis: x in {|[0,(- 1)]|,|[0,1]|}
then x in P2 by XBOOLE_0:def 4;
then x in P by A5, XBOOLE_0:def 3;
then consider q being Point of (TOP-REAL 2) such that
A9: q = x and
A10: |.q.| = 1 by A3;
x in Q by A8, XBOOLE_0:def 4;
then A11: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 = 0 ) ;
then (0 ^2) + ((q `2) ^2) = 1 ^2 by A9, A10, JGRAPH_3:1;
then ( q `2 = 1 or q `2 = - 1 ) by SQUARE_1:41;
then ( x = |[0,(- 1)]| or x = |[0,1]| ) by A11, A9, EUCLID:53;
hence x in {|[0,(- 1)]|,|[0,1]|} by TARSKI:def 2; :: thesis: verum

end;

A12: for p being Point of (TOP-REAL 2) holds h2 . p = proj2 . p ;
reconsider R = Lower_Arc P as non empty Subset of (TOP-REAL 2) ;
A13: Vertical_Line 0 is closed by JORDAN6:30;
A14: Vertical_Line 0 is closed by JORDAN6:30;
A15: for p being Point of (TOP-REAL 2) holds h2 . p = proj2 . p ;
A16: ( S-bound P = - 1 & N-bound P = 1 ) by A3, Th28;
A17: ( W-bound P = - 1 & E-bound P = 1 ) by A3, Th28;
then A18: P1 meets Q by A4, A16, A1, JORDAN6:70, XBOOLE_1:64;
A19: P2 meets Q by A4, A17, A16, A1, JORDAN6:69, XBOOLE_1:64;
A20: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by A4, JORDAN6:def 9;
A21: Lower_Arc P is_an_arc_of E-max P, W-min P by A4, JORDAN6:def 9;
then consider f being Function of I[01],((TOP-REAL 2) | R) such that
A22: f is being_homeomorphism and
A23: f . 0 = E-max P and
A24: f . 1 = W-min P by TOPREAL1:def 1;
A25: ( dom f = the carrier of I[01] & dom h2 = the carrier of (TOP-REAL 2) ) by FUNCT_2:def 1;
A26: rng f = [#] ((TOP-REAL 2) | R) by A22, TOPS_2:def 5
.= R by PRE_TOPC:def 5 ;
A27: Upper_Arc P c= P by A5, XBOOLE_1:7;
A28: rng (h2 * f) c= the carrier of R^1 ;
A29: the carrier of ((TOP-REAL 2) | R) = R by PRE_TOPC:8;
then rng f c= the carrier of (TOP-REAL 2) by XBOOLE_1:1;
then dom (h2 * f) = the carrier of I[01] by A25, RELAT_1:27;
then reconsider g0 = h2 * f as Function of I[01],R^1 by A28, FUNCT_2:2;
A30: f is one-to-one by A22, TOPS_2:def 5;
A31: f is continuous by A22, TOPS_2:def 5;
A32: ( ex p being Point of (TOP-REAL 2) ex t being Real st
( 0 < t & t < 1 & f . t = p & p `2 < 0 ) implies for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
q `2 <= 0 )

proof

given p being Point of (TOP-REAL 2), t being Real such that A33: 0 < t and
A34: t < 1 and
A35: f . t = p and
A36: p `2 < 0 ; :: thesis: for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
q `2 <= 0

now :: thesis: for q being Point of (TOP-REAL 2) holds
( not q in Lower_Arc P or not q `2 > 0 )

assume ex q being Point of (TOP-REAL 2) st
( q in Lower_Arc P & q `2 > 0 ) ; :: thesis: contradiction
then consider q being Point of (TOP-REAL 2) such that
A37: q in Lower_Arc P and
A38: q `2 > 0 ;
rng f = [#] ((TOP-REAL 2) | R) by A22, TOPS_2:def 5
.= R by PRE_TOPC:def 5 ;
then consider x being object such that
A39: x in dom f and
A40: q = f . x by A37, FUNCT_1:def 3;
A41: dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then A42: x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A39, RCOMP_1:def 1;
t in { v where v is Real : ( 0 <= v & v <= 1 ) } by A33, A34;
then A43: t in [.0,1.] by RCOMP_1:def 1;
then A44: (h2 * f) . t = h2 . p by A35, A41, FUNCT_1:13
.= p `2 by PSCOMP_1:def 6 ;
consider r being Real such that
A45: x = r and
A46: 0 <= r and
A47: r <= 1 by A42;
A48: (h2 * f) . r = h2 . q by A39, A40, A45, FUNCT_1:13
.= q `2 by PSCOMP_1:def 6 ;

now :: thesis: ( ( r < t & contradiction ) or ( t < r & contradiction ) or ( t = r & contradiction ) )

per cases ( r < t or t < r or t = r ) by XXREAL_0:1;

case A49: r < t ; :: thesis: contradiction

then reconsider B = [.r,t.] as non empty Subset of I[01] by A39, A45, A43, BORSUK_1:40, XXREAL_1:1, XXREAL_2:def 12;
reconsider B0 = B as Subset of I[01] ;
reconsider g = g0 | B0 as Function of (I[01] | B0),R^1 by PRE_TOPC:9;
A50: (q `2) * (p `2) < 0 by A36, A38, XREAL_1:132;
t in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) } by A49;
then t in B by RCOMP_1:def 1;
then A51: p `2 = g . t by A44, FUNCT_1:49;
r in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) } by A49;
then r in B by RCOMP_1:def 1;
then A52: q `2 = g . r by A48, FUNCT_1:49;
g0 is continuous by A31, A12, Th7, Th32;
then A53: g is continuous by TOPMETR:7;
Closed-Interval-TSpace (r,t) = I[01] | B by A34, A46, A49, TOPMETR:20, TOPMETR:23;
then consider r1 being Real such that
A54: g . r1 = 0 and
A55: r < r1 and
A56: r1 < t by A49, A53, A50, A52, A51, TOPREAL5:8;
r1 in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) } by A55, A56;
then A57: r1 in B by RCOMP_1:def 1;
r1 < 1 by A34, A56, XXREAL_0:2;
then r1 in { r2 where r2 is Real : ( 0 <= r2 & r2 <= 1 ) } by A46, A55;
then A58: r1 in dom f by A41, RCOMP_1:def 1;
then f . r1 in rng f by FUNCT_1:def 3;
then f . r1 in R by A29;
then f . r1 in P by A6;
then consider q3 being Point of (TOP-REAL 2) such that
A59: q3 = f . r1 and
A60: |.q3.| = 1 by A3;
A61: q3 `2 = h2 . (f . r1) by A59, PSCOMP_1:def 6
.= (h2 * f) . r1 by A58, FUNCT_1:13
.= 0 by A54, A57, FUNCT_1:49 ;
then A62: 1 ^2 = ((q3 `1) ^2) + (0 ^2) by A60, JGRAPH_3:1
.= (q3 `1) ^2 ;

now :: thesis: ( ( q3 `1 = 1 & contradiction ) or ( q3 `1 = - 1 & contradiction ) )

per cases ( q3 `1 = 1 or q3 `1 = - 1 ) by A62, SQUARE_1:41;

case A63: q3 `1 = 1 ; :: thesis: contradiction

A64: 0 in dom f by A41, XXREAL_1:1;
q3 = |[1,0]| by A61, A63, EUCLID:53
.= E-max P by A3, Th30 ;
hence contradiction by A23, A30, A46, A55, A58, A59, A64, FUNCT_1:def 4; :: thesis: verum

end;

case A65: q3 `1 = - 1 ; :: thesis: contradiction

A66: 1 in dom f by A41, XXREAL_1:1;
q3 = |[(- 1),0]| by A61, A65, EUCLID:53
.= W-min P by A3, Th29 ;
hence contradiction by A24, A30, A34, A56, A58, A59, A66, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A67: t < r ; :: thesis: contradiction

then reconsider B = [.t,r.] as non empty Subset of I[01] by A39, A45, A43, BORSUK_1:40, XXREAL_1:1, XXREAL_2:def 12;
reconsider B0 = B as Subset of I[01] ;
reconsider g = g0 | B0 as Function of (I[01] | B0),R^1 by PRE_TOPC:9;
A68: (q `2) * (p `2) < 0 by A36, A38, XREAL_1:132;
t in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) } by A67;
then t in B by RCOMP_1:def 1;
then A69: p `2 = g . t by A44, FUNCT_1:49;
r in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) } by A67;
then r in B by RCOMP_1:def 1;
then A70: q `2 = g . r by A48, FUNCT_1:49;
g0 is continuous by A31, A12, Th7, Th32;
then A71: g is continuous by TOPMETR:7;
Closed-Interval-TSpace (t,r) = I[01] | B by A33, A47, A67, TOPMETR:20, TOPMETR:23;
then consider r1 being Real such that
A72: g . r1 = 0 and
A73: t < r1 and
A74: r1 < r by A67, A71, A68, A70, A69, TOPREAL5:8;
r1 in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) } by A73, A74;
then A75: r1 in B by RCOMP_1:def 1;
r1 < 1 by A47, A74, XXREAL_0:2;
then r1 in { r2 where r2 is Real : ( 0 <= r2 & r2 <= 1 ) } by A33, A73;
then A76: r1 in dom f by A41, RCOMP_1:def 1;
then f . r1 in rng f by FUNCT_1:def 3;
then f . r1 in R by A29;
then f . r1 in P by A6;
then consider q3 being Point of (TOP-REAL 2) such that
A77: q3 = f . r1 and
A78: |.q3.| = 1 by A3;
A79: q3 `2 = h2 . (f . r1) by A77, PSCOMP_1:def 6
.= (h2 * f) . r1 by A76, FUNCT_1:13
.= 0 by A72, A75, FUNCT_1:49 ;
then A80: 1 ^2 = ((q3 `1) ^2) + (0 ^2) by A78, JGRAPH_3:1
.= (q3 `1) ^2 ;

now :: thesis: ( ( q3 `1 = 1 & contradiction ) or ( q3 `1 = - 1 & contradiction ) )

per cases ( q3 `1 = 1 or q3 `1 = - 1 ) by A80, SQUARE_1:41;

case A81: q3 `1 = 1 ; :: thesis: contradiction

A82: 0 in dom f by A41, XXREAL_1:1;
q3 = |[1,0]| by A79, A81, EUCLID:53
.= E-max P by A3, Th30 ;
hence contradiction by A23, A30, A33, A73, A76, A77, A82, FUNCT_1:def 4; :: thesis: verum

end;

case A83: q3 `1 = - 1 ; :: thesis: contradiction

A84: 1 in dom f by A41, XXREAL_1:1;
q3 = |[(- 1),0]| by A79, A83, EUCLID:53
.= W-min P by A3, Th29 ;
hence contradiction by A24, A30, A47, A74, A76, A77, A84, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case t = r ; :: thesis: contradiction

hence contradiction by A36, A38, A48, A44; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
q `2 <= 0 ; :: thesis: verum

end;

reconsider R = Upper_Arc P as non empty Subset of (TOP-REAL 2) ;
A85: Upper_Arc P is_an_arc_of W-min P, E-max P by A4, JORDAN6:def 8;
then consider f2 being Function of I[01],((TOP-REAL 2) | R) such that
A86: f2 is being_homeomorphism and
A87: f2 . 0 = W-min P and
A88: f2 . 1 = E-max P by TOPREAL1:def 1;
A89: ( dom f2 = the carrier of I[01] & dom h2 = the carrier of (TOP-REAL 2) ) by FUNCT_2:def 1;
A90: rng (h2 * f2) c= the carrier of R^1 ;
A91: the carrier of ((TOP-REAL 2) | R) = R by PRE_TOPC:8;
then rng f2 c= the carrier of (TOP-REAL 2) by XBOOLE_1:1;
then dom (h2 * f2) = the carrier of I[01] by A89, RELAT_1:27;
then reconsider g1 = h2 * f2 as Function of I[01],R^1 by A90, FUNCT_2:2;
A92: f2 is one-to-one by A86, TOPS_2:def 5;
A93: f2 is continuous by A86, TOPS_2:def 5;
A94: ( ex p being Point of (TOP-REAL 2) ex t being Real st
( 0 < t & t < 1 & f2 . t = p & p `2 < 0 ) implies for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
q `2 <= 0 )

proof

given p being Point of (TOP-REAL 2), t being Real such that A95: 0 < t and
A96: t < 1 and
A97: f2 . t = p and
A98: p `2 < 0 ; :: thesis: for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
q `2 <= 0

now :: thesis: for q being Point of (TOP-REAL 2) holds
( not q in Upper_Arc P or not q `2 > 0 )

assume ex q being Point of (TOP-REAL 2) st
( q in Upper_Arc P & q `2 > 0 ) ; :: thesis: contradiction
then consider q being Point of (TOP-REAL 2) such that
A99: q in Upper_Arc P and
A100: q `2 > 0 ;
rng f2 = [#] ((TOP-REAL 2) | R) by A86, TOPS_2:def 5
.= R by PRE_TOPC:def 5 ;
then consider x being object such that
A101: x in dom f2 and
A102: q = f2 . x by A99, FUNCT_1:def 3;
A103: dom f2 = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then A104: x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A101, RCOMP_1:def 1;
t in { v where v is Real : ( 0 <= v & v <= 1 ) } by A95, A96;
then A105: t in [.0,1.] by RCOMP_1:def 1;
then A106: (h2 * f2) . t = h2 . p by A97, A103, FUNCT_1:13
.= p `2 by PSCOMP_1:def 6 ;
consider r being Real such that
A107: x = r and
A108: 0 <= r and
A109: r <= 1 by A104;
A110: (h2 * f2) . r = h2 . q by A101, A102, A107, FUNCT_1:13
.= q `2 by PSCOMP_1:def 6 ;

now :: thesis: ( ( r < t & contradiction ) or ( t < r & contradiction ) or ( t = r & contradiction ) )

per cases ( r < t or t < r or t = r ) by XXREAL_0:1;

case A111: r < t ; :: thesis: contradiction

then reconsider B = [.r,t.] as non empty Subset of I[01] by A101, A107, A105, BORSUK_1:40, XXREAL_1:1, XXREAL_2:def 12;
reconsider B0 = B as Subset of I[01] ;
reconsider g = g1 | B0 as Function of (I[01] | B0),R^1 by PRE_TOPC:9;
A112: (q `2) * (p `2) < 0 by A98, A100, XREAL_1:132;
t in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) } by A111;
then t in B by RCOMP_1:def 1;
then A113: p `2 = g . t by A106, FUNCT_1:49;
r in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) } by A111;
then r in B by RCOMP_1:def 1;
then A114: q `2 = g . r by A110, FUNCT_1:49;
g1 is continuous by A93, A15, Th7, Th32;
then A115: g is continuous by TOPMETR:7;
Closed-Interval-TSpace (r,t) = I[01] | B by A96, A108, A111, TOPMETR:20, TOPMETR:23;
then consider r1 being Real such that
A116: g . r1 = 0 and
A117: r < r1 and
A118: r1 < t by A111, A115, A112, A114, A113, TOPREAL5:8;
r1 in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) } by A117, A118;
then A119: r1 in B by RCOMP_1:def 1;
r1 < 1 by A96, A118, XXREAL_0:2;
then r1 in { r2 where r2 is Real : ( 0 <= r2 & r2 <= 1 ) } by A108, A117;
then A120: r1 in dom f2 by A103, RCOMP_1:def 1;
then f2 . r1 in rng f2 by FUNCT_1:def 3;
then f2 . r1 in R by A91;
then f2 . r1 in P by A27;
then consider q3 being Point of (TOP-REAL 2) such that
A121: q3 = f2 . r1 and
A122: |.q3.| = 1 by A3;
A123: q3 `2 = h2 . (f2 . r1) by A121, PSCOMP_1:def 6
.= (h2 * f2) . r1 by A120, FUNCT_1:13
.= 0 by A116, A119, FUNCT_1:49 ;
then A124: 1 ^2 = ((q3 `1) ^2) + (0 ^2) by A122, JGRAPH_3:1
.= (q3 `1) ^2 ;

now :: thesis: ( ( q3 `1 = 1 & contradiction ) or ( q3 `1 = - 1 & contradiction ) )

per cases ( q3 `1 = 1 or q3 `1 = - 1 ) by A124, SQUARE_1:41;

case A125: q3 `1 = 1 ; :: thesis: contradiction

A126: 1 in dom f2 by A103, XXREAL_1:1;
q3 = |[1,0]| by A123, A125, EUCLID:53
.= E-max P by A3, Th30 ;
hence contradiction by A88, A92, A96, A118, A120, A121, A126, FUNCT_1:def 4; :: thesis: verum

end;

case A127: q3 `1 = - 1 ; :: thesis: contradiction

A128: 0 in dom f2 by A103, XXREAL_1:1;
q3 = |[(- 1),0]| by A123, A127, EUCLID:53
.= W-min P by A3, Th29 ;
hence contradiction by A87, A92, A108, A117, A120, A121, A128, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A129: t < r ; :: thesis: contradiction

then reconsider B = [.t,r.] as non empty Subset of I[01] by A101, A107, A105, BORSUK_1:40, XXREAL_1:1, XXREAL_2:def 12;
reconsider B0 = B as Subset of I[01] ;
reconsider g = g1 | B0 as Function of (I[01] | B0),R^1 by PRE_TOPC:9;
A130: (q `2) * (p `2) < 0 by A98, A100, XREAL_1:132;
t in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) } by A129;
then t in B by RCOMP_1:def 1;
then A131: p `2 = g . t by A106, FUNCT_1:49;
r in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) } by A129;
then r in B by RCOMP_1:def 1;
then A132: q `2 = g . r by A110, FUNCT_1:49;
g1 is continuous by A93, A15, Th7, Th32;
then A133: g is continuous by TOPMETR:7;
Closed-Interval-TSpace (t,r) = I[01] | B by A95, A109, A129, TOPMETR:20, TOPMETR:23;
then consider r1 being Real such that
A134: g . r1 = 0 and
A135: t < r1 and
A136: r1 < r by A129, A133, A130, A132, A131, TOPREAL5:8;
r1 in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) } by A135, A136;
then A137: r1 in B by RCOMP_1:def 1;
r1 < 1 by A109, A136, XXREAL_0:2;
then r1 in { r2 where r2 is Real : ( 0 <= r2 & r2 <= 1 ) } by A95, A135;
then A138: r1 in dom f2 by A103, RCOMP_1:def 1;
then f2 . r1 in rng f2 by FUNCT_1:def 3;
then f2 . r1 in R by A91;
then f2 . r1 in P by A27;
then consider q3 being Point of (TOP-REAL 2) such that
A139: q3 = f2 . r1 and
A140: |.q3.| = 1 by A3;
A141: q3 `2 = h2 . (f2 . r1) by A139, PSCOMP_1:def 6
.= (h2 * f2) . r1 by A138, FUNCT_1:13
.= 0 by A134, A137, FUNCT_1:49 ;
then A142: 1 ^2 = ((q3 `1) ^2) + (0 ^2) by A140, JGRAPH_3:1
.= (q3 `1) ^2 ;

now :: thesis: ( ( q3 `1 = 1 & contradiction ) or ( q3 `1 = - 1 & contradiction ) )

per cases ( q3 `1 = 1 or q3 `1 = - 1 ) by A142, SQUARE_1:41;

case A143: q3 `1 = 1 ; :: thesis: contradiction

A144: 1 in dom f2 by A103, XXREAL_1:1;
q3 = |[1,0]| by A141, A143, EUCLID:53
.= E-max P by A3, Th30 ;
hence contradiction by A88, A92, A109, A136, A138, A139, A144, FUNCT_1:def 4; :: thesis: verum

end;

case A145: q3 `1 = - 1 ; :: thesis: contradiction

A146: 0 in dom f2 by A103, XXREAL_1:1;
q3 = |[(- 1),0]| by A141, A145, EUCLID:53
.= W-min P by A3, Th29 ;
hence contradiction by A87, A92, A95, A135, A138, A139, A146, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case t = r ; :: thesis: contradiction

hence contradiction by A98, A100, A110, A106; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
q `2 <= 0 ; :: thesis: verum

end;

A147: ( W-bound P = - 1 & E-bound P = 1 ) by A3, Th28;
Lower_Arc P is closed by A21, JORDAN6:11;
then P1 /\ Q is closed by A13, TOPS_1:8;
then A148: Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0)) in P1 /\ Q by A21, A18, JORDAN5C:def 2;
then Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0)) in P1 by XBOOLE_0:def 4;
then consider x8 being object such that
A149: x8 in dom f and
A150: Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0)) = f . x8 by A26, FUNCT_1:def 3;
dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then x8 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A149, RCOMP_1:def 1;
then consider r8 being Real such that
A151: x8 = r8 and
A152: 0 <= r8 and
A153: r8 <= 1 ;
P1 /\ Q c= {|[0,(- 1)]|,|[0,1]|}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 /\ Q or x in {|[0,(- 1)]|,|[0,1]|} )
assume A154: x in P1 /\ Q ; :: thesis: x in {|[0,(- 1)]|,|[0,1]|}
then x in P1 by XBOOLE_0:def 4;
then x in P by A5, XBOOLE_0:def 3;
then consider q being Point of (TOP-REAL 2) such that
A155: q = x and
A156: |.q.| = 1 by A3;
x in Q by A154, XBOOLE_0:def 4;
then A157: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 = 0 ) ;
then (0 ^2) + ((q `2) ^2) = 1 ^2 by A155, A156, JGRAPH_3:1;
then ( q `2 = 1 or q `2 = - 1 ) by SQUARE_1:41;
then ( x = |[0,(- 1)]| or x = |[0,1]| ) by A157, A155, EUCLID:53;
hence x in {|[0,(- 1)]|,|[0,1]|} by TARSKI:def 2; :: thesis: verum

end;

then ( Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0)) = |[0,(- 1)]| or Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0)) = |[0,1]| ) by A148, TARSKI:def 2;
then A158: ( (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0))) `2 = - 1 or (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0))) `2 = 1 ) by EUCLID:52;

A159: now :: thesis: not r8 = 0

assume r8 = 0 ; :: thesis: contradiction
then Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0)) = |[1,0]| by A3, A23, A150, A151, Th30;
hence contradiction by A158, EUCLID:52; :: thesis: verum

end;

Upper_Arc P is closed by A85, JORDAN6:11;
then P2 /\ Q is closed by A14, TOPS_1:8;
then First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0)) in P2 /\ Q by A85, A19, JORDAN5C:def 1;
then A160: ( First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0)) = |[0,(- 1)]| or First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0)) = |[0,1]| ) by A7, TARSKI:def 2;
W-min P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A161: W-min P in Lower_Arc P by A20, XBOOLE_0:def 4;
A162: (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A4, JORDAN6:def 9;

now :: thesis: not r8 = 1

assume r8 = 1 ; :: thesis: contradiction
then Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0)) = |[(- 1),0]| by A3, A24, A150, A151, Th29;
hence contradiction by A158, EUCLID:52; :: thesis: verum

end;

then A163: 1 > r8 by A153, XXREAL_0:1;
E-max P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A164: E-max P in Lower_Arc P by A20, XBOOLE_0:def 4;
A165: { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } c= Lower_Arc P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } or x in Lower_Arc P )
assume x in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } ; :: thesis: x in Lower_Arc P
then consider p being Point of (TOP-REAL 2) such that
A166: p = x and
A167: p in P and
A168: p `2 <= 0 ;

now :: thesis: ( ( p `2 = 0 & x in Lower_Arc P ) or ( p `2 < 0 & x in Lower_Arc P ) )

per cases ( p `2 = 0 or p `2 < 0 ) by A168;

case A169: p `2 = 0 ; :: thesis: x in Lower_Arc P

ex p8 being Point of (TOP-REAL 2) st
( p8 = p & |.p8.| = 1 ) by A3, A167;
then 1 = sqrt (((p `1) ^2) + ((p `2) ^2)) by JGRAPH_3:1
.= |.(p `1).| by A169, COMPLEX1:72 ;
then ( p = |[(p `1),(p `2)]| & (p `1) ^2 = 1 ^2 ) by COMPLEX1:75, EUCLID:53;
then ( p = |[1,0]| or p = |[(- 1),0]| ) by A169, SQUARE_1:41;
hence x in Lower_Arc P by A3, A164, A161, A166, Th29, Th30; :: thesis: verum

end;

case A170: p `2 < 0 ; :: thesis: x in Lower_Arc P

now :: thesis: x in Lower_Arc P

assume not x in Lower_Arc P ; :: thesis: contradiction
then A171: x in Upper_Arc P by A5, A166, A167, XBOOLE_0:def 3;
rng f2 = [#] ((TOP-REAL 2) | R) by A86, TOPS_2:def 5
.= R by PRE_TOPC:def 5 ;
then consider x2 being object such that
A172: x2 in dom f2 and
A173: p = f2 . x2 by A166, A171, FUNCT_1:def 3;
dom f2 = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then x2 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A172, RCOMP_1:def 1;
then consider t2 being Real such that
A174: x2 = t2 and
A175: 0 <= t2 and
A176: t2 <= 1 ;
A177: |[0,1]| `2 = 1 by EUCLID:52;

now :: thesis: not t2 = 1

assume t2 = 1 ; :: thesis: contradiction
then p = |[1,0]| by A3, A88, A173, A174, Th30;
hence contradiction by A170, EUCLID:52; :: thesis: verum

end;

then A178: t2 < 1 by A176, XXREAL_0:1;

A179: now :: thesis: not t2 = 0

assume t2 = 0 ; :: thesis: contradiction
then p = |[(- 1),0]| by A3, A87, A173, A174, Th29;
hence contradiction by A170, EUCLID:52; :: thesis: verum

end;

|[0,1]| `1 = 0 by EUCLID:52;
then |.|[0,1]|.| = sqrt ((0 ^2) + (1 ^2)) by A177, JGRAPH_3:1
.= 1 ;
then A180: |[0,1]| in { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } ;

now :: thesis: ( ( |[0,1]| in Lower_Arc P & contradiction ) or ( |[0,1]| in Upper_Arc P & contradiction ) )

per cases ( |[0,1]| in Lower_Arc P or |[0,1]| in Upper_Arc P ) by A3, A5, A180, XBOOLE_0:def 3;

case |[0,1]| in Lower_Arc P ; :: thesis: contradiction

hence contradiction by A162, A147, A158, A160, A150, A151, A152, A159, A163, A32, A177, EUCLID:52; :: thesis: verum

end;

case |[0,1]| in Upper_Arc P ; :: thesis: contradiction

hence contradiction by A94, A170, A173, A174, A175, A179, A178, A177; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence x in Lower_Arc P ; :: thesis: verum

end;

end;

end;

hence x in Lower_Arc P ; :: thesis: verum

end;

Lower_Arc P c= { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) }

proof

let x2 be object ; :: according to TARSKI:def 3 :: thesis: ( not x2 in Lower_Arc P or x2 in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } )
assume A181: x2 in Lower_Arc P ; :: thesis: x2 in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) }
then reconsider q3 = x2 as Point of (TOP-REAL 2) ;
q3 `2 <= 0 by A162, A147, A158, A160, A150, A151, A152, A159, A163, A32, A181, EUCLID:52;
hence x2 in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A6, A181; :: thesis: verum

end;

hence Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A165, XBOOLE_0:def 10; :: thesis: verum