:: JORDAN6 semantic presentation

theorem :: JORDAN6:1

canceled;

theorem Th2: :: JORDAN6:2

for r, s being real number st r <= s holds
( r <= (r + s) / 2 & (r + s) / 2 <= s )

proof end;

theorem Th3: :: JORDAN6:3

for TX being non empty TopSpace
for P being Subset of TX
for A being Subset of (TX | P)
for B being Subset of TX st B is closed & A = B /\ P holds
A is closed

proof end;

theorem Th4: :: JORDAN6:4

for TX, TY being non empty TopSpace
for P being non empty Subset of TY
for f being Function of TX,(TY | P) holds
( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds
f2 is continuous ) )

proof end;

theorem Th5: :: JORDAN6:5

for r being real number
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 >= r } holds
P is closed

proof end;

theorem Th6: :: JORDAN6:6

for r being real number
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 <= r } holds
P is closed

proof end;

theorem Th7: :: JORDAN6:7

for r being real number
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 = r } holds
P is closed

proof end;

theorem Th8: :: JORDAN6:8

for r being real number
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 >= r } holds
P is closed

proof end;

theorem Th9: :: JORDAN6:9

for r being real number
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 <= r } holds
P is closed

proof end;

theorem Th10: :: JORDAN6:10

for r being real number
for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 = r } holds
P is closed

proof end;

theorem Th11: :: JORDAN6:11

for n being Nat
for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
P is connected

proof end;

theorem Th12: :: JORDAN6:12

for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
P is closed

proof end;

theorem Th13: :: JORDAN6:13

for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
ex q being Point of (TOP-REAL 2) st
( q in P & q `1 = ((p1 `1 ) + (p2 `1 )) / 2 )

proof end;

theorem Th14: :: JORDAN6:14

for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1 ) + (p2 `1 )) / 2 } holds
( P meets Q & P /\ Q is closed )

proof end;

theorem Th15: :: JORDAN6:15

for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2 ) + (p2 `2 )) / 2 } holds
( P meets Q & P /\ Q is closed )

proof end;

definition

let P be Subset of (TOP-REAL 2);
let p1, p2 be Point of (TOP-REAL 2);
func x_Middle P,p1,p2 -> Point of (TOP-REAL 2) means :Def1: :: JORDAN6:def 1
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
it = First_Point P,p1,p2,Q;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines x_Middle JORDAN6:def 1 :

definition

let P be Subset of (TOP-REAL 2);
let p1, p2 be Point of (TOP-REAL 2);
func y_Middle P,p1,p2 -> Point of (TOP-REAL 2) means :Def2: :: JORDAN6:def 2
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
it = First_Point P,p1,p2,Q;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines y_Middle JORDAN6:def 2 :

theorem :: JORDAN6:16

for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
( x_Middle P,p1,p2 in P & y_Middle P,p1,p2 in P )

proof end;

theorem :: JORDAN6:17

for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
( p1 = x_Middle P,p1,p2 iff p1 `1 = p2 `1 )

proof end;

theorem :: JORDAN6:18

for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
( p1 = y_Middle P,p1,p2 iff p1 `2 = p2 `2 )

proof end;

theorem Th19: :: JORDAN6:19

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

proof end;

definition

let P be Subset of (TOP-REAL 2);
let p1, p2, q1 be Point of (TOP-REAL 2);
func L_Segment P,p1,p2,q1 -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 3
{ q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } ;
coherence

proof end;

end;

:: deftheorem defines L_Segment JORDAN6:def 3 :

definition

let P be Subset of (TOP-REAL 2);
let p1, p2, q1 be Point of (TOP-REAL 2);
func R_Segment P,p1,p2,q1 -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 4
{ q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ;
coherence

proof end;

end;

:: deftheorem defines R_Segment JORDAN6:def 4 :

theorem Th20: :: JORDAN6:20

for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) holds L_Segment P,p1,p2,q1 c= P

proof end;

theorem Th21: :: JORDAN6:21

for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) holds R_Segment P,p1,p2,q1 c= P

proof end;

theorem :: JORDAN6:22

for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
L_Segment P,p1,p2,p1 = {p1}

proof end;

theorem :: JORDAN6:23

canceled;

theorem :: JORDAN6:24

canceled;

theorem :: JORDAN6:25

for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
L_Segment P,p1,p2,p2 = P

proof end;

theorem :: JORDAN6:26

for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
R_Segment P,p1,p2,p2 = {p2}

proof end;

theorem :: JORDAN6:27

for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
R_Segment P,p1,p2,p1 = P

proof end;

theorem :: JORDAN6:28

for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P holds
R_Segment P,p1,p2,q1 = L_Segment P,p2,p1,q1

proof end;

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 :: JORDAN6:def 5
(R_Segment P,p1,p2,q1) /\ (L_Segment P,p1,p2,q2);
correctness ;

end;

:: deftheorem defines Segment JORDAN6:def 5 :

theorem :: JORDAN6:29

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 ) }

proof end;

theorem Th30: :: JORDAN6:30

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
( LE q1,q2,P,p1,p2 iff LE q2,q1,P,p2,p1 )

proof end;

theorem Th31: :: JORDAN6:31

for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q in P holds
L_Segment P,p1,p2,q = R_Segment P,p2,p1,q

proof end;

theorem :: JORDAN6:32

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 & q1 in P & q2 in P holds
Segment P,p1,p2,q1,q2 = Segment P,p2,p1,q2,q1

proof end;

definition

let s be real number ;
func Vertical_Line s -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 6
{ p where p is Point of (TOP-REAL 2) : p `1 = s } ;
correctness

proof end;

func Horizontal_Line s -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 7
{ p where p is Point of (TOP-REAL 2) : p `2 = s } ;
correctness

proof end;

end;

:: deftheorem defines Vertical_Line JORDAN6:def 6 :

:: deftheorem defines Horizontal_Line JORDAN6:def 7 :

theorem Th33: :: JORDAN6:33

for r being real number holds
( Vertical_Line r is closed & Horizontal_Line r is closed ) by Th7, Th10;

theorem Th34: :: JORDAN6:34

for r being real number
for p being Point of (TOP-REAL 2) holds
( p in Vertical_Line r iff p `1 = r )

proof end;

theorem :: JORDAN6:35

for r being real number
for p being Point of (TOP-REAL 2) holds
( p in Horizontal_Line r iff p `2 = r )

proof end;

theorem :: JORDAN6:36

canceled;

theorem :: JORDAN6:37

canceled;

theorem :: JORDAN6:38

canceled;

theorem :: JORDAN6:39

canceled;

theorem Th40: :: JORDAN6:40

for P being Subset of (TOP-REAL 2) st P is_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 )

proof end;

theorem Th41: :: JORDAN6:41

for P being Subset of I[01] st P = the carrier of I[01] \ {0,1} holds
P is open

proof end;

Lm1: for r, s being real number holds ].r,s.[ misses {r,s}
by RCOMP_1:46;

Lm2: for a, b, c being real number holds
( c in ].a,b.[ iff ( a < c & c < b ) )
by RCOMP_1:47;

theorem :: JORDAN6:42

canceled;

theorem :: JORDAN6:43

canceled;

theorem :: JORDAN6:44

canceled;

theorem :: JORDAN6:45

canceled;

theorem :: JORDAN6:46

for P being Subset of R^1
for r, s being real number st P = ].r,s.[ holds
P is open

proof end;

theorem Th47: :: JORDAN6:47

for S being TopSpace
for P1, P2 being Subset of S
for P1' being Subset of (S | P2) st P1 = P1' & P1 c= P2 holds
S | P1 = (S | P2) | P1'

proof end;

theorem Th48: :: JORDAN6:48

for P7 being Subset of I[01] st P7 = the carrier of I[01] \ {0,1} holds
( P7 <> {} & P7 is connected )

proof end;

theorem Th49: :: JORDAN6:49

for n being Nat
for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
p1 <> p2

proof end;

theorem :: JORDAN6:50

for n being Nat
for P being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is open

proof end;

theorem :: JORDAN6:51

canceled;

theorem Th52: :: JORDAN6:52

for n being Nat
for P, P1, P2 being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds
Q is open

proof end;

theorem Th53: :: JORDAN6:53

for n being Nat
for P being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is connected

proof end;

theorem Th54: :: JORDAN6:54

for GX being TopSpace
for P1, P being Subset of GX
for Q' being Subset of (GX | P1)
for Q being Subset of (GX | P) st P1 c= P & Q = Q' & Q' is connected holds
Q is connected

proof end;

theorem Th55: :: JORDAN6:55

for n being Nat
for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
ex p3 being Point of (TOP-REAL n) st
( p3 in P & p3 <> p1 & p3 <> p2 )

proof end;

theorem :: JORDAN6:56

for n being Nat
for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
P \ {p1,p2} <> {}

proof end;

theorem :: JORDAN6:57

for n being Nat
for P1, P being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} holds
Q is connected

proof end;

theorem Th58: :: JORDAN6:58

for T, S, V being non empty TopSpace
for P1 being non empty Subset of S
for P2 being Subset of S
for f being Function of T,(S | P1)
for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds
ex h being Function of T,V st
( h = g * f & h is continuous )

proof end;

theorem Th59: :: JORDAN6:59

for n being Nat
for P1, P2 being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds
P1 = P2

proof end;

theorem Th60: :: JORDAN6:60

for P being Subset of (TOP-REAL 2)
for Q being Subset of ((TOP-REAL 2) | P)
for p1, p2 being Point of (TOP-REAL 2) st P is_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} holds
not Q is connected

proof end;

theorem Th61: :: JORDAN6:61

for P, P1, P2, P1', P2' being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1' is_an_arc_of p1,p2 & P2' is_an_arc_of p1,p2 & P1' \/ P2' = P & not ( P1 = P1' & P2 = P2' ) holds
( P1 = P2' & P2 = P1' )

proof end;

registration

cluster -> real Element of the carrier of R^1 ;
coherence by TOPMETR:24, XREAL_0:def 1;

end;

Lm3: 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] & s1 = g . 0 & s2 = g . 1 holds
ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = r )

proof end;

theorem :: JORDAN6:62

canceled;

theorem :: JORDAN6:63

canceled;

theorem Th64: :: JORDAN6:64

for P1 being Subset of (TOP-REAL 2)
for r being real number
for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 holds
( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )

proof end;

Lm4: now

let P be Simple_closed_curve; :: thesis:
let P1, P1' be non empty Subset of (TOP-REAL 2); :: thesis:
assume 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 ) & 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 ) ) ; :: thesis:
then consider P2 being non empty Subset of (TOP-REAL 2) such that
A2: ( 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 ) ;
A3: P2 is_an_arc_of W-min P, E-max P by A2, JORDAN5B:14;
consider P2' being non empty Subset of (TOP-REAL 2) such that
A4: ( 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 ) by A1;
A5: P2' is_an_arc_of W-min P, E-max P by A4, JORDAN5B:14;

now

assume A6: ( P1 = P2' & P2 = P1' ) ; :: thesis:
A7: (W-min P) `1 = W-bound P by PSCOMP_1:84;
A8: (E-max P) `1 = E-bound P by PSCOMP_1:104;
then (W-min P) `1 < (E-max P) `1 by A7, TOPREAL5:23;
then A9: ( (W-min P) `1 <= ((W-bound P) + (E-bound P)) / 2 & ((W-bound P) + (E-bound P)) / 2 <= (E-max P) `1 ) by A7, A8, TOPREAL3:3;
then ( P2 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) & P2 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed ) by A3, Th64;
then A10: (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 A2, JORDAN5C:18;
( P2' meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) & P2' /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed ) by A5, A9, Th64;
hence contradiction by A4, A6, A10, JORDAN5C:18; :: thesis:

end;

hence P1 = P1' by A2, A3, A4, A5, Th61; :: thesis:

end;

definition

let P be Subset of (TOP-REAL 2);
assume A1: P is_simple_closed_curve ;
func Upper_Arc P -> non empty Subset of (TOP-REAL 2) means :Def8: :: JORDAN6:def 8
( it 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 & it /\ P2 = {(W-min P),(E-max P)} & it \/ P2 = P & (First_Point it,(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 ) );
existence

proof end;

uniqueness by A1, Lm4;

end;

:: deftheorem Def8 defines Upper_Arc JORDAN6:def 8 :

definition

let P be Subset of (TOP-REAL 2);
assume A1: P is_simple_closed_curve ;
then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by Def8;
func Lower_Arc P -> non empty Subset of (TOP-REAL 2) means :Def9: :: JORDAN6:def 9
( it is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ it = {(W-min P),(E-max P)} & (Upper_Arc P) \/ it = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point it,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 );
existence by A1, Def8;
uniqueness

proof end;

end;

:: deftheorem Def9 defines Lower_Arc JORDAN6:def 9 :

theorem Th65: :: JORDAN6:65

for P being Subset of (TOP-REAL 2) st P is_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 )

proof end;

theorem Th66: :: JORDAN6:66

for P being Subset of (TOP-REAL 2) st P is_simple_closed_curve holds
( Lower_Arc P = (P \ (Upper_Arc P)) \/ {(W-min P),(E-max P)} & Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} )

proof end;

theorem :: JORDAN6:67

for P being Subset of (TOP-REAL 2)
for P1 being Subset of ((TOP-REAL 2) | P) st P is_simple_closed_curve & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P holds
P1 = Lower_Arc P

proof end;

theorem :: JORDAN6:68

for P being Subset of (TOP-REAL 2)
for P1 being Subset of ((TOP-REAL 2) | P) st P is_simple_closed_curve & P1 /\ (Lower_Arc P) = {(W-min P),(E-max P)} & P1 \/ (Lower_Arc P) = P holds
P1 = Upper_Arc P

proof end;

theorem Th69: :: JORDAN6:69

for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 holds
q = p1

proof end;

theorem Th70: :: JORDAN6:70

for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 holds
q = p2

proof end;

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: :: JORDAN6:def 10
( ( 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 :

theorem :: JORDAN6:71

for P being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st P is_simple_closed_curve & q in P holds
LE q,q,P

proof end;

theorem :: JORDAN6:72

for P being Subset of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) st P is_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds
q1 = q2

proof end;

theorem :: JORDAN6:73

for P being Subset of (TOP-REAL 2)
for q1, q2, q3 being Point of (TOP-REAL 2) st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P holds
LE q1,q3,P

proof end;