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 Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } )
assume A1:
P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 }
; :: thesis: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
then A2:
P is being_simple_closed_curve
by JGRAPH_3:36;
then A3:
Upper_Arc P is_an_arc_of W-min P, E-max P
by JORDAN6:def 8;
A4:
Lower_Arc P is_an_arc_of E-max P, W-min P
by A2, JORDAN6:def 9;
consider P2 being non empty Subset of (TOP-REAL 2) such that
A5:
( P2 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ P2 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P2 = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 )
by A2, JORDAN6:def 8;
set P4 = Lower_Arc P;
A6:
( Lower_Arc P is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (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 A2, JORDAN6:def 9;
A7:
W-bound P = - 1
by A1, Th31;
A8:
E-bound P = 1
by A1, Th31;
set P1 = Upper_Arc P;
set P2 = Lower_Arc P;
set Q = Vertical_Line 0 ;
set p11 = W-min P;
set p22 = E-max P;
set p8 = First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0 );
set pj = Last_Point (Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0 );
A9:
W-bound P = - 1
by A1, Th31;
A10:
E-bound P = 1
by A1, Th31;
A11:
S-bound P = - 1
by A1, Th31;
A12:
N-bound P = 1
by A1, Th31;
A13:
LSeg |[0 ,(- 1)]|,|[0 ,1]| c= Vertical_Line 0
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in LSeg |[0 ,(- 1)]|,|[0 ,1]| or x in Vertical_Line 0 )
assume
x in LSeg |[0 ,(- 1)]|,
|[0 ,1]|
;
:: thesis: x in Vertical_Line 0
then
x in { (((1 - l) * |[0 ,(- 1)]|) + (l * |[0 ,1]|)) where l is Real : ( 0 <= l & l <= 1 ) }
;
then consider l being
Real such that A14:
(
x = ((1 - l) * |[0 ,(- 1)]|) + (l * |[0 ,1]|) &
0 <= l &
l <= 1 )
;
(((1 - l) * |[0 ,(- 1)]|) + (l * |[0 ,1]|)) `1 =
(((1 - l) * |[0 ,(- 1)]|) `1 ) + ((l * |[0 ,1]|) `1 )
by TOPREAL3:7
.=
((1 - l) * (|[0 ,(- 1)]| `1 )) + ((l * |[0 ,1]|) `1 )
by TOPREAL3:9
.=
((1 - l) * (|[0 ,(- 1)]| `1 )) + (l * (|[0 ,1]| `1 ))
by TOPREAL3:9
.=
((1 - l) * 0 ) + (l * (|[0 ,1]| `1 ))
by EUCLID:56
.=
((1 - l) * 0 ) + (l * 0 )
by EUCLID:56
.=
0
;
hence
x in Vertical_Line 0
by A14;
:: thesis: verum
end;
then A15:
Upper_Arc P meets Vertical_Line 0
by A2, A9, A10, A11, A12, JORDAN6:84, XBOOLE_1:64;
A16:
Upper_Arc P is closed
by A3, JORDAN6:12;
Vertical_Line 0 is closed
by JORDAN6:33;
then
(Upper_Arc P) /\ (Vertical_Line 0 ) is closed
by A16, TOPS_1:35;
then A17:
( First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0 ) in (Upper_Arc P) /\ (Vertical_Line 0 ) & ( for g being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc P))
for s2 being Real st g is being_homeomorphism & g . 0 = W-min P & g . 1 = E-max P & g . s2 = First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0 ) & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Vertical_Line 0 ) )
by A3, A15, JORDAN5C:def 1;
(Upper_Arc P) /\ (Vertical_Line 0 ) c= {|[0 ,(- 1)]|,|[0 ,1]|}
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (Upper_Arc P) /\ (Vertical_Line 0 ) or x in {|[0 ,(- 1)]|,|[0 ,1]|} )
assume
x in (Upper_Arc P) /\ (Vertical_Line 0 )
;
:: thesis: x in {|[0 ,(- 1)]|,|[0 ,1]|}
then A18:
(
x in Upper_Arc P &
x in Vertical_Line 0 )
by XBOOLE_0:def 4;
then consider p being
Point of
(TOP-REAL 2) such that A19:
(
p = x &
p `1 = 0 )
;
x in P
by A5, A18, XBOOLE_0:def 3;
then consider q being
Point of
(TOP-REAL 2) such that A20:
(
q = x &
|.q.| = 1 )
by A1;
(0 ^2 ) + ((q `2 ) ^2 ) = 1
^2
by A19, A20, JGRAPH_3:10;
then
(
q `2 = 1 or
q `2 = - 1 )
by SQUARE_1:110;
then
(
x = |[0 ,(- 1)]| or
x = |[0 ,1]| )
by A19, A20, EUCLID:57;
hence
x in {|[0 ,(- 1)]|,|[0 ,1]|}
by TARSKI:def 2;
:: thesis: verum
end;
then
( 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 A17, TARSKI:def 2;
then A21:
( (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0 )) `2 = - 1 or (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0 )) `2 = 1 )
by EUCLID:56;
A22:
Lower_Arc P meets Vertical_Line 0
by A2, A9, A10, A11, A12, A13, JORDAN6:85, XBOOLE_1:64;
A23:
Lower_Arc P is closed
by A4, JORDAN6:12;
Vertical_Line 0 is closed
by JORDAN6:33;
then
(Lower_Arc P) /\ (Vertical_Line 0 ) is closed
by A23, TOPS_1:35;
then A24:
( Last_Point (Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0 ) in (Lower_Arc P) /\ (Vertical_Line 0 ) & ( for g being Function of I[01] ,((TOP-REAL 2) | (Lower_Arc P))
for s2 being Real st g is being_homeomorphism & g . 0 = E-max P & g . 1 = W-min P & g . s2 = Last_Point (Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0 ) & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Vertical_Line 0 ) )
by A4, A22, JORDAN5C:def 2;
(Lower_Arc P) /\ (Vertical_Line 0 ) c= {|[0 ,(- 1)]|,|[0 ,1]|}
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (Lower_Arc P) /\ (Vertical_Line 0 ) or x in {|[0 ,(- 1)]|,|[0 ,1]|} )
assume
x in (Lower_Arc P) /\ (Vertical_Line 0 )
;
:: thesis: x in {|[0 ,(- 1)]|,|[0 ,1]|}
then A25:
(
x in Lower_Arc P &
x in Vertical_Line 0 )
by XBOOLE_0:def 4;
then consider p being
Point of
(TOP-REAL 2) such that A26:
(
p = x &
p `1 = 0 )
;
x in P
by A6, A25, XBOOLE_0:def 3;
then consider q being
Point of
(TOP-REAL 2) such that A27:
(
q = x &
|.q.| = 1 )
by A1;
(0 ^2 ) + ((q `2 ) ^2 ) = 1
^2
by A26, A27, JGRAPH_3:10;
then
(
q `2 = 1 or
q `2 = - 1 )
by SQUARE_1:110;
then
(
x = |[0 ,(- 1)]| or
x = |[0 ,1]| )
by A26, A27, EUCLID:57;
hence
x in {|[0 ,(- 1)]|,|[0 ,1]|}
by TARSKI:def 2;
:: thesis: verum
end;
then A28:
( 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 A24, TARSKI:def 2;
A29:
First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0 ) in Upper_Arc P
by A17, XBOOLE_0:def 4;
A30:
Upper_Arc P c= P
by A5, XBOOLE_1:7;
A31:
Lower_Arc P c= P
by A6, XBOOLE_1:7;
E-max P in {(W-min P),(E-max P)}
by TARSKI:def 2;
then A32:
E-max P in Upper_Arc P
by A5, XBOOLE_0:def 4;
W-min P in {(W-min P),(E-max P)}
by TARSKI:def 2;
then A33:
W-min P in Upper_Arc P
by A5, XBOOLE_0:def 4;
reconsider R = Upper_Arc P as non empty Subset of (TOP-REAL 2) ;
consider f being Function of I[01] ,((TOP-REAL 2) | R) such that
A34:
( f is being_homeomorphism & f . 0 = W-min P & f . 1 = E-max P )
by A3, TOPREAL1:def 2;
rng f =
[#] ((TOP-REAL 2) | R)
by A34, TOPS_2:def 5
.=
R
by PRE_TOPC:def 10
;
then consider x8 being set such that
A35:
( x8 in dom f & First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0 ) = f . x8 )
by A29, FUNCT_1:def 5;
dom f = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then
x8 in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A35, RCOMP_1:def 1;
then consider r8 being Real such that
A36:
( x8 = r8 & 0 <= r8 & r8 <= 1 )
;
then A38:
1 > r8
by A36, XXREAL_0:1;
reconsider h2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
A39:
f is continuous
by A34, TOPS_2:def 5;
A40:
f is one-to-one
by A34, TOPS_2:def 5;
for p being Point of (TOP-REAL 2) holds h2 . p = proj2 . p
;
then A41:
h2 is continuous
by Th35;
A42:
dom f = the carrier of I[01]
by FUNCT_2:def 1;
A43:
the carrier of ((TOP-REAL 2) | R) = R
by PRE_TOPC:29;
then A44:
rng f c= the carrier of (TOP-REAL 2)
by XBOOLE_1:1;
dom h2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
then A45:
dom (h2 * f) = the carrier of I[01]
by A42, A44, RELAT_1:46;
rng (h2 * f) c= the carrier of R^1
;
then reconsider g0 = h2 * f as Function of I[01] ,R^1 by A45, FUNCT_2:4;
A46:
( 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 Upper_Arc P holds
q `2 >= 0 )
proof
assume
ex
p being
Point of
(TOP-REAL 2) ex
t being
Real st
(
0 < t &
t < 1 &
f . t = p &
p `2 > 0 )
;
:: thesis: for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
q `2 >= 0
then consider p being
Point of
(TOP-REAL 2),
t being
Real such that A47:
(
0 < t &
t < 1 &
f . t = p &
p `2 > 0 )
;
now assume
ex
q being
Point of
(TOP-REAL 2) st
(
q in Upper_Arc P &
q `2 < 0 )
;
:: thesis: contradictionthen consider q being
Point of
(TOP-REAL 2) such that A48:
(
q in Upper_Arc P &
q `2 < 0 )
;
rng f =
[#] ((TOP-REAL 2) | R)
by A34, TOPS_2:def 5
.=
R
by PRE_TOPC:def 10
;
then consider x being
set such that A49:
(
x in dom f &
q = f . x )
by A48, FUNCT_1:def 5;
A50:
dom f = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then
x in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A49, RCOMP_1:def 1;
then consider r being
Real such that A51:
(
x = r &
0 <= r &
r <= 1 )
;
A52:
(h2 * f) . r =
h2 . q
by A49, A51, FUNCT_1:23
.=
q `2
by PSCOMP_1:def 29
;
t in { v where v is Real : ( 0 <= v & v <= 1 ) }
by A47;
then A53:
t in [.0 ,1.]
by RCOMP_1:def 1;
then A54:
(h2 * f) . t =
h2 . p
by A47, A50, FUNCT_1:23
.=
p `2
by PSCOMP_1:def 29
;
now per cases
( r < t or t < r or t = r )
by XXREAL_0:1;
case A55:
r < t
;
:: thesis: contradictionthen reconsider B =
[.r,t.] as non
empty Subset of
I[01] by A49, A51, A53, BORSUK_1:83, 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:30;
g0 is
continuous
by A39, A41, Th10;
then A56:
g is
continuous
by TOPMETR:10;
A57:
Closed-Interval-TSpace r,
t = I[01] | B
by A47, A51, A55, TOPMETR:27, TOPMETR:30;
r in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) }
by A55;
then A58:
r in B
by RCOMP_1:def 1;
t in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) }
by A55;
then
t in B
by RCOMP_1:def 1;
then
(
(q `2 ) * (p `2 ) < 0 &
q `2 = g . r &
p `2 = g . t )
by A47, A48, A52, A54, A58, FUNCT_1:72, XREAL_1:134;
then consider r1 being
Real such that A59:
(
g . r1 = 0 &
r < r1 &
r1 < t )
by A55, A56, A57, TOPREAL5:14;
r1 in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) }
by A59;
then A60:
r1 in B
by RCOMP_1:def 1;
r1 < 1
by A47, A59, XXREAL_0:2;
then
r1 in { r2 where r2 is Real : ( 0 <= r2 & r2 <= 1 ) }
by A51, A59;
then A61:
r1 in dom f
by A50, RCOMP_1:def 1;
then
f . r1 in rng f
by FUNCT_1:def 5;
then
f . r1 in R
by A43;
then
f . r1 in P
by A30;
then consider q3 being
Point of
(TOP-REAL 2) such that A62:
(
q3 = f . r1 &
|.q3.| = 1 )
by A1;
A63:
q3 `2 =
h2 . (f . r1)
by A62, PSCOMP_1:def 29
.=
g0 . r1
by A61, FUNCT_1:23
.=
0
by A59, A60, FUNCT_1:72
;
then A64: 1
^2 =
((q3 `1 ) ^2 ) + (0 ^2 )
by A62, JGRAPH_3:10
.=
(q3 `1 ) ^2
;
now per cases
( q3 `1 = 1 or q3 `1 = - 1 )
by A64, SQUARE_1:110;
case
q3 `1 = 1
;
:: thesis: contradictionthen A65:
q3 =
|[1,0 ]|
by A63, EUCLID:57
.=
E-max P
by A1, Th33
;
1
in dom f
by A50, XXREAL_1:1;
hence
contradiction
by A34, A40, A47, A59, A61, A62, A65, FUNCT_1:def 8;
:: thesis: verum end; case
q3 `1 = - 1
;
:: thesis: contradictionthen A66:
q3 =
|[(- 1),0 ]|
by A63, EUCLID:57
.=
W-min P
by A1, Th32
;
0 in dom f
by A50, XXREAL_1:1;
hence
contradiction
by A34, A40, A51, A59, A61, A62, A66, FUNCT_1:def 8;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end; case A67:
t < r
;
:: thesis: contradictionthen reconsider B =
[.t,r.] as non
empty Subset of
I[01] by A49, A51, A53, BORSUK_1:83, 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:30;
g0 is
continuous
by A39, A41, Th10;
then A68:
g is
continuous
by TOPMETR:10;
A69:
Closed-Interval-TSpace t,
r = I[01] | B
by A47, A51, A67, TOPMETR:27, TOPMETR:30;
r in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) }
by A67;
then A70:
r in B
by RCOMP_1:def 1;
t in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) }
by A67;
then
t in B
by RCOMP_1:def 1;
then
(
(q `2 ) * (p `2 ) < 0 &
q `2 = g . r &
p `2 = g . t )
by A47, A48, A52, A54, A70, FUNCT_1:72, XREAL_1:134;
then consider r1 being
Real such that A71:
(
g . r1 = 0 &
t < r1 &
r1 < r )
by A67, A68, A69, TOPREAL5:14;
r1 in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) }
by A71;
then A72:
r1 in B
by RCOMP_1:def 1;
r1 < 1
by A51, A71, XXREAL_0:2;
then
r1 in { r2 where r2 is Real : ( 0 <= r2 & r2 <= 1 ) }
by A47, A71;
then A73:
r1 in dom f
by A50, RCOMP_1:def 1;
then
f . r1 in rng f
by FUNCT_1:def 5;
then
f . r1 in R
by A43;
then
f . r1 in P
by A30;
then consider q3 being
Point of
(TOP-REAL 2) such that A74:
(
q3 = f . r1 &
|.q3.| = 1 )
by A1;
A75:
q3 `2 =
h2 . (f . r1)
by A74, PSCOMP_1:def 29
.=
(h2 * f) . r1
by A73, FUNCT_1:23
.=
0
by A71, A72, FUNCT_1:72
;
then A76: 1
^2 =
((q3 `1 ) ^2 ) + (0 ^2 )
by A74, JGRAPH_3:10
.=
(q3 `1 ) ^2
;
now per cases
( q3 `1 = 1 or q3 `1 = - 1 )
by A76, SQUARE_1:110;
case
q3 `1 = 1
;
:: thesis: contradictionthen A77:
q3 =
|[1,0 ]|
by A75, EUCLID:57
.=
E-max P
by A1, Th33
;
1
in dom f
by A50, XXREAL_1:1;
hence
contradiction
by A34, A40, A51, A71, A73, A74, A77, FUNCT_1:def 8;
:: thesis: verum end; case
q3 `1 = - 1
;
:: thesis: contradictionthen A78:
q3 =
|[(- 1),0 ]|
by A75, EUCLID:57
.=
W-min P
by A1, Th32
;
0 in dom f
by A50, XXREAL_1:1;
hence
contradiction
by A34, A40, A47, A71, A73, A74, A78, FUNCT_1:def 8;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum 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;
reconsider R = Lower_Arc P as non empty Subset of (TOP-REAL 2) ;
consider f2 being Function of I[01] ,((TOP-REAL 2) | R) such that
A79:
( f2 is being_homeomorphism & f2 . 0 = E-max P & f2 . 1 = W-min P )
by A4, TOPREAL1:def 2;
A80:
f2 is continuous
by A79, TOPS_2:def 5;
A81:
f2 is one-to-one
by A79, TOPS_2:def 5;
for p being Point of (TOP-REAL 2) holds h2 . p = proj2 . p
;
then A82:
h2 is continuous
by Th35;
A83:
dom f2 = the carrier of I[01]
by FUNCT_2:def 1;
A84:
the carrier of ((TOP-REAL 2) | R) = R
by PRE_TOPC:29;
then A85:
rng f2 c= the carrier of (TOP-REAL 2)
by XBOOLE_1:1;
dom h2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
then A86:
dom (h2 * f2) = the carrier of I[01]
by A83, A85, RELAT_1:46;
rng (h2 * f2) c= the carrier of R^1
;
then reconsider g1 = h2 * f2 as Function of I[01] ,R^1 by A86, FUNCT_2:4;
A87:
( 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 Lower_Arc P holds
q `2 >= 0 )
proof
assume
ex
p being
Point of
(TOP-REAL 2) ex
t being
Real st
(
0 < t &
t < 1 &
f2 . t = p &
p `2 > 0 )
;
:: thesis: for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
q `2 >= 0
then consider p being
Point of
(TOP-REAL 2),
t being
Real such that A88:
(
0 < t &
t < 1 &
f2 . t = p &
p `2 > 0 )
;
now assume
ex
q being
Point of
(TOP-REAL 2) st
(
q in Lower_Arc P &
q `2 < 0 )
;
:: thesis: contradictionthen consider q being
Point of
(TOP-REAL 2) such that A89:
(
q in Lower_Arc P &
q `2 < 0 )
;
rng f2 =
[#] ((TOP-REAL 2) | R)
by A79, TOPS_2:def 5
.=
R
by PRE_TOPC:def 10
;
then consider x being
set such that A90:
(
x in dom f2 &
q = f2 . x )
by A89, FUNCT_1:def 5;
A91:
dom f2 = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then
x in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A90, RCOMP_1:def 1;
then consider r being
Real such that A92:
(
x = r &
0 <= r &
r <= 1 )
;
A93:
(h2 * f2) . r =
h2 . q
by A90, A92, FUNCT_1:23
.=
q `2
by PSCOMP_1:def 29
;
t in { v where v is Real : ( 0 <= v & v <= 1 ) }
by A88;
then A94:
t in [.0 ,1.]
by RCOMP_1:def 1;
then A95:
(h2 * f2) . t =
h2 . p
by A88, A91, FUNCT_1:23
.=
p `2
by PSCOMP_1:def 29
;
now per cases
( r < t or t < r or t = r )
by XXREAL_0:1;
case A96:
r < t
;
:: thesis: contradictionthen reconsider B =
[.r,t.] as non
empty Subset of
I[01] by A90, A92, A94, BORSUK_1:83, 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:30;
g1 is
continuous
by A80, A82, Th10;
then A97:
g is
continuous
by TOPMETR:10;
A98:
Closed-Interval-TSpace r,
t = I[01] | B
by A88, A92, A96, TOPMETR:27, TOPMETR:30;
r in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) }
by A96;
then A99:
r in B
by RCOMP_1:def 1;
t in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) }
by A96;
then
t in B
by RCOMP_1:def 1;
then
(
(q `2 ) * (p `2 ) < 0 &
q `2 = g . r &
p `2 = g . t )
by A88, A89, A93, A95, A99, FUNCT_1:72, XREAL_1:134;
then consider r1 being
Real such that A100:
(
g . r1 = 0 &
r < r1 &
r1 < t )
by A96, A97, A98, TOPREAL5:14;
r1 in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) }
by A100;
then A101:
r1 in B
by RCOMP_1:def 1;
r1 < 1
by A88, A100, XXREAL_0:2;
then
r1 in { r2 where r2 is Real : ( 0 <= r2 & r2 <= 1 ) }
by A92, A100;
then A102:
r1 in dom f2
by A91, RCOMP_1:def 1;
then
f2 . r1 in rng f2
by FUNCT_1:def 5;
then
f2 . r1 in R
by A84;
then
f2 . r1 in P
by A31;
then consider q3 being
Point of
(TOP-REAL 2) such that A103:
(
q3 = f2 . r1 &
|.q3.| = 1 )
by A1;
A104:
q3 `2 =
h2 . (f2 . r1)
by A103, PSCOMP_1:def 29
.=
(h2 * f2) . r1
by A102, FUNCT_1:23
.=
0
by A100, A101, FUNCT_1:72
;
then A105: 1
^2 =
((q3 `1 ) ^2 ) + (0 ^2 )
by A103, JGRAPH_3:10
.=
(q3 `1 ) ^2
;
now per cases
( q3 `1 = 1 or q3 `1 = - 1 )
by A105, SQUARE_1:110;
case
q3 `1 = 1
;
:: thesis: contradictionthen A106:
q3 =
|[1,0 ]|
by A104, EUCLID:57
.=
E-max P
by A1, Th33
;
0 in dom f2
by A91, XXREAL_1:1;
hence
contradiction
by A79, A81, A92, A100, A102, A103, A106, FUNCT_1:def 8;
:: thesis: verum end; case
q3 `1 = - 1
;
:: thesis: contradictionthen A107:
q3 =
|[(- 1),0 ]|
by A104, EUCLID:57
.=
W-min P
by A1, Th32
;
1
in dom f2
by A91, XXREAL_1:1;
hence
contradiction
by A79, A81, A88, A100, A102, A103, A107, FUNCT_1:def 8;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end; case A108:
t < r
;
:: thesis: contradictionthen reconsider B =
[.t,r.] as non
empty Subset of
I[01] by A90, A92, A94, BORSUK_1:83, 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:30;
g1 is
continuous
by A80, A82, Th10;
then A109:
g is
continuous
by TOPMETR:10;
A110:
Closed-Interval-TSpace t,
r = I[01] | B
by A88, A92, A108, TOPMETR:27, TOPMETR:30;
r in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) }
by A108;
then A111:
r in B
by RCOMP_1:def 1;
t in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) }
by A108;
then
t in B
by RCOMP_1:def 1;
then
(
(q `2 ) * (p `2 ) < 0 &
q `2 = g . r &
p `2 = g . t )
by A88, A89, A93, A95, A111, FUNCT_1:72, XREAL_1:134;
then consider r1 being
Real such that A112:
(
g . r1 = 0 &
t < r1 &
r1 < r )
by A108, A109, A110, TOPREAL5:14;
r1 in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) }
by A112;
then A113:
r1 in B
by RCOMP_1:def 1;
r1 < 1
by A92, A112, XXREAL_0:2;
then
r1 in { r2 where r2 is Real : ( 0 <= r2 & r2 <= 1 ) }
by A88, A112;
then A114:
r1 in dom f2
by A91, RCOMP_1:def 1;
then
f2 . r1 in rng f2
by FUNCT_1:def 5;
then
f2 . r1 in R
by A84;
then
f2 . r1 in P
by A31;
then consider q3 being
Point of
(TOP-REAL 2) such that A115:
(
q3 = f2 . r1 &
|.q3.| = 1 )
by A1;
A116:
q3 `2 =
h2 . (f2 . r1)
by A115, PSCOMP_1:def 29
.=
g1 . r1
by A114, FUNCT_1:23
.=
0
by A112, A113, FUNCT_1:72
;
then A117: 1
^2 =
((q3 `1 ) ^2 ) + (0 ^2 )
by A115, JGRAPH_3:10
.=
(q3 `1 ) ^2
;
now per cases
( q3 `1 = 1 or q3 `1 = - 1 )
by A117, SQUARE_1:110;
case
q3 `1 = 1
;
:: thesis: contradictionthen A118:
q3 =
|[1,0 ]|
by A116, EUCLID:57
.=
E-max P
by A1, Th33
;
0 in dom f2
by A91, XXREAL_1:1;
hence
contradiction
by A79, A81, A88, A112, A114, A115, A118, FUNCT_1:def 8;
:: thesis: verum end; case
q3 `1 = - 1
;
:: thesis: contradictionthen A119:
q3 =
|[(- 1),0 ]|
by A116, EUCLID:57
.=
W-min P
by A1, Th32
;
1
in dom f2
by A91, XXREAL_1:1;
hence
contradiction
by A79, A81, A92, A112, A114, A115, A119, FUNCT_1:def 8;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum 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;
A120:
Upper_Arc P c= { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
proof
let x2 be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x2 in Upper_Arc P or x2 in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } )
assume A121:
x2 in Upper_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 A6, A7, A8, A21, A28, A35, A36, A37, A38, A46, A121, EUCLID:56;
hence
x2 in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
by A30, A121;
:: thesis: verum
end;
{ p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } c= Upper_Arc P
proof
let x be
set ;
:: 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 Upper_Arc P )
assume
x in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
;
:: thesis: x in Upper_Arc P
then consider p being
Point of
(TOP-REAL 2) such that A122:
(
p = x &
p in P &
p `2 >= 0 )
;
now per cases
( p `2 = 0 or p `2 > 0 )
by A122;
case A123:
p `2 = 0
;
:: thesis: x in Upper_Arc Pconsider p8 being
Point of
(TOP-REAL 2) such that A124:
(
p8 = p &
|.p8.| = 1 )
by A1, A122;
A125:
p = |[(p `1 ),(p `2 )]|
by EUCLID:57;
1 =
sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 ))
by A124, JGRAPH_3:10
.=
abs (p `1 )
by A123, COMPLEX1:158
;
then
(p `1 ) ^2 = 1
^2
by COMPLEX1:161;
then
(
p = |[1,0 ]| or
p = |[(- 1),0 ]| )
by A123, A125, SQUARE_1:110;
hence
x in Upper_Arc P
by A1, A32, A33, A122, Th32, Th33;
:: thesis: verum end; case A126:
p `2 > 0
;
:: thesis: x in Upper_Arc Pnow assume
not
x in Upper_Arc P
;
:: thesis: contradictionthen A127:
x in Lower_Arc P
by A6, A122, XBOOLE_0:def 3;
rng f2 =
[#] ((TOP-REAL 2) | R)
by A79, TOPS_2:def 5
.=
R
by PRE_TOPC:def 10
;
then consider x2 being
set such that A128:
(
x2 in dom f2 &
p = f2 . x2 )
by A122, A127, FUNCT_1:def 5;
dom f2 = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then
x2 in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A128, RCOMP_1:def 1;
then consider t2 being
Real such that A129:
(
x2 = t2 &
0 <= t2 &
t2 <= 1 )
;
then A131:
(
0 < t2 &
t2 < 1 &
f2 . t2 = p &
p `2 > 0 )
by A126, A128, A129, A130, XXREAL_0:1;
A132:
|[0 ,(- 1)]| `1 = 0
by EUCLID:56;
A133:
|[0 ,(- 1)]| `2 = - 1
by EUCLID:56;
then |.|[0 ,(- 1)]|.| =
sqrt ((0 ^2 ) + ((- 1) ^2 ))
by A132, JGRAPH_3:10
.=
1
by SQUARE_1:83
;
then A134:
|[0 ,(- 1)]| in { q where q is Point of (TOP-REAL 2) : |.q.| = 1 }
;
now per cases
( |[0 ,(- 1)]| in Upper_Arc P or |[0 ,(- 1)]| in Lower_Arc P )
by A1, A6, A134, XBOOLE_0:def 3;
case
|[0 ,(- 1)]| in Upper_Arc P
;
:: thesis: contradictionhence
contradiction
by A6, A7, A8, A21, A28, A35, A36, A37, A38, A46, A133, EUCLID:56;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end; hence
x in Upper_Arc P
;
:: thesis: verum
hence
x in Upper_Arc P
;
:: thesis: verum
end;
hence
Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
by A120, XBOOLE_0:def 10; :: thesis: verum