begin
definition
let P be
Subset of
(TOP-REAL 2);
let p1,
p2 be
Point of
(TOP-REAL 2);
existence
ex b1 being Point of (TOP-REAL 2) st
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
b1 = First_Point (P,p1,p2,Q)
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
b1 = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
b2 = First_Point (P,p1,p2,Q) ) holds
b1 = b2
end;
definition
let P be
Subset of
(TOP-REAL 2);
let p1,
p2 be
Point of
(TOP-REAL 2);
existence
ex b1 being Point of (TOP-REAL 2) st
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
b1 = First_Point (P,p1,p2,Q)
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
b1 = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
b2 = First_Point (P,p1,p2,Q) ) holds
b1 = b2
end;
begin
theorem Th18:
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
LE q1,
q2,
P,
p1,
p2 holds
LE q2,
q1,
P,
p2,
p1
definition
let P be
Subset of
(TOP-REAL 2);
let p1,
p2,
q1,
q2 be
Point of
(TOP-REAL 2);
func Segment (
P,
p1,
p2,
q1,
q2)
-> Subset of
(TOP-REAL 2) equals
(R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2));
correctness
coherence
(R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2)) is Subset of (TOP-REAL 2);
;
end;
::
deftheorem defines
Segment JORDAN6:def 5 :
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (P,p1,p2,q1,q2) = (R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2));
theorem
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) holds
Segment (
P,
p1,
p2,
q1,
q2)
= { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
theorem
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
LE q2,
q1,
P,
p2,
p1 holds
LE q1,
q2,
P,
p1,
p2 by Th18, JORDAN5B:14;
theorem
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 holds
Segment (
P,
p1,
p2,
q1,
q2)
= Segment (
P,
p2,
p1,
q2,
q1)
begin
theorem Th33:
for
P being
Subset of
(TOP-REAL 2) st
P is
being_simple_closed_curve holds
ex
P1,
P2 being non
empty Subset of
(TOP-REAL 2) st
(
P1 is_an_arc_of W-min P,
E-max P &
P2 is_an_arc_of E-max P,
W-min P &
P1 /\ P2 = {(W-min P),(E-max P)} &
P1 \/ P2 = P &
(First_Point (P1,(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 )
begin
begin
Lm1:
for g being Function of I[01],R^1
for s1, s2, r being real number st g is continuous & g . 0[01] < r & r < g . 1[01] holds
ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r )
Lm2:
now for P being Simple_closed_curve
for P1, P19 being non empty Subset of (TOP-REAL 2) st ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(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 ) & ex P29 being non empty Subset of (TOP-REAL 2) st
( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) holds
P1 = P19
let P be
Simple_closed_curve;
for P1, P19 being non empty Subset of (TOP-REAL 2) st ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(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 ) & ex P29 being non empty Subset of (TOP-REAL 2) st
( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) holds
P1 = P19let P1,
P19 be non
empty Subset of
(TOP-REAL 2);
( ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(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 ) & ex P29 being non empty Subset of (TOP-REAL 2) st
( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) implies P1 = P19 )assume that A1:
ex
P2 being non
empty Subset of
(TOP-REAL 2) st
(
P1 is_an_arc_of W-min P,
E-max P &
P2 is_an_arc_of E-max P,
W-min P &
P1 /\ P2 = {(W-min P),(E-max P)} &
P1 \/ P2 = P &
(First_Point (P1,(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 )
and A2:
ex
P29 being non
empty Subset of
(TOP-REAL 2) st
(
P19 is_an_arc_of W-min P,
E-max P &
P29 is_an_arc_of E-max P,
W-min P &
P19 /\ P29 = {(W-min P),(E-max P)} &
P19 \/ P29 = P &
(First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
;
P1 = P19consider P2 being non
empty Subset of
(TOP-REAL 2) such that A3:
P1 is_an_arc_of W-min P,
E-max P
and A4:
P2 is_an_arc_of E-max P,
W-min P
and
P1 /\ P2 = {(W-min P),(E-max P)}
and A5:
P1 \/ P2 = P
and A6:
(First_Point (P1,(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 A1;
A7:
P2 is_an_arc_of W-min P,
E-max P
by A4, JORDAN5B:14;
consider P29 being non
empty Subset of
(TOP-REAL 2) such that A8:
P19 is_an_arc_of W-min P,
E-max P
and A9:
P29 is_an_arc_of E-max P,
W-min P
and
P19 /\ P29 = {(W-min P),(E-max P)}
and A10:
P19 \/ P29 = P
and A11:
(First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2
by A2;
A12:
P29 is_an_arc_of W-min P,
E-max P
by A9, JORDAN5B:14;
now ( P1 = P29 implies not P2 = P19 )
assume that A13:
P1 = P29
and A14:
P2 = P19
;
contradictionA15:
(W-min P) `1 = W-bound P
by EUCLID:52;
A16:
(E-max P) `1 = E-bound P
by EUCLID:52;
then A17:
(W-min P) `1 < (E-max P) `1
by A15, TOPREAL5:17;
then A18:
(W-min P) `1 <= ((W-bound P) + (E-bound P)) / 2
by A15, A16, XREAL_1:226;
A19:
((W-bound P) + (E-bound P)) / 2
<= (E-max P) `1
by A15, A16, A17, XREAL_1:226;
then A20:
P2 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2)
by A7, A18, Th49;
P2 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is
closed
by A7, A18, A19, Th49;
then A21:
(First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (First_Point (P2,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2
by A4, A6, A20, JORDAN5C:18;
A22:
P29 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2)
by A12, A18, A19, Th49;
P29 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is
closed
by A12, A18, A19, Th49;
hence
contradiction
by A9, A11, A13, A14, A21, A22, JORDAN5C:18;
verum
end;
hence
P1 = P19
by A3, A5, A7, A8, A10, A12, Th48;
verum
end;
definition
let P be
Subset of
(TOP-REAL 2);
assume A1:
P is
being_simple_closed_curve
;
existence
ex b1 being non empty Subset of (TOP-REAL 2) st
( b1 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & b1 /\ P2 = {(W-min P),(E-max P)} & b1 \/ P2 = P & (First_Point (b1,(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 ) )
uniqueness
for b1, b2 being non empty Subset of (TOP-REAL 2) st b1 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & b1 /\ P2 = {(W-min P),(E-max P)} & b1 \/ P2 = P & (First_Point (b1,(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 ) & b2 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & b2 /\ P2 = {(W-min P),(E-max P)} & b2 \/ P2 = P & (First_Point (b2,(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 ) holds
b1 = b2
by A1, Lm2;
end;
definition
let P be
Subset of
(TOP-REAL 2);
assume A1:
P is
being_simple_closed_curve
;
then A2:
Upper_Arc P is_an_arc_of W-min P,
E-max P
by Def8;
existence
ex b1 being non empty Subset of (TOP-REAL 2) st
( b1 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b1 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
by A1, Def8;
uniqueness
for b1, b2 being non empty Subset of (TOP-REAL 2) st b1 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b1 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 & b2 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b2 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b2 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 holds
b1 = b2
end;
theorem Th50:
for
P being
Subset of
(TOP-REAL 2) st
P is
being_simple_closed_curve holds
(
Upper_Arc P is_an_arc_of W-min P,
E-max P &
Upper_Arc P is_an_arc_of E-max P,
W-min P &
Lower_Arc P is_an_arc_of E-max P,
W-min P &
Lower_Arc P is_an_arc_of W-min P,
E-max 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 )
begin
definition
let P be
Subset of
(TOP-REAL 2);
let q1,
q2 be
Point of
(TOP-REAL 2);
pred LE q1,
q2,
P means :
Def10:
( (
q1 in Upper_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P ) or (
q1 in Upper_Arc P &
q2 in Upper_Arc P &
LE q1,
q2,
Upper_Arc P,
W-min P,
E-max P ) or (
q1 in Lower_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P &
LE q1,
q2,
Lower_Arc P,
E-max P,
W-min P ) );
end;
::
deftheorem Def10 defines
LE JORDAN6:def 10 :
for P being Subset of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) holds
( LE q1,q2,P iff ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) );