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