:: JORDAN6 semantic presentation

theorem Th1: :: JORDAN6:1
canceled;

theorem Th2: :: JORDAN6:2
for b1, b2 being real number st b1 <= b2 holds
( b1 <= (b1 + b2) / 2 & (b1 + b2) / 2 <= b2 )
proof end;

theorem Th3: :: JORDAN6:3
for b1 being non empty TopSpace
for b2 being Subset of b1
for b3 being Subset of (b1 | b2)
for b4 being Subset of b1 st b4 is closed & b3 = b4 /\ b2 holds
b3 is closed
proof end;

theorem Th4: :: JORDAN6:4
for b1, b2 being non empty TopSpace
for b3 being non empty Subset of b2
for b4 being Function of b1,(b2 | b3) holds
( b4 is Function of b1,b2 & ( for b5 being Function of b1,b2 st b5 = b4 & b4 is continuous holds
b5 is continuous ) )
proof end;

theorem Th5: :: JORDAN6:5
for b1 being real number
for b2 being Subset of (TOP-REAL 2) st b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `1 >= b1 } holds
b2 is closed
proof end;

theorem Th6: :: JORDAN6:6
for b1 being real number
for b2 being Subset of (TOP-REAL 2) st b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `1 <= b1 } holds
b2 is closed
proof end;

theorem Th7: :: JORDAN6:7
for b1 being real number
for b2 being Subset of (TOP-REAL 2) st b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `1 = b1 } holds
b2 is closed
proof end;

theorem Th8: :: JORDAN6:8
for b1 being real number
for b2 being Subset of (TOP-REAL 2) st b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 >= b1 } holds
b2 is closed
proof end;

theorem Th9: :: JORDAN6:9
for b1 being real number
for b2 being Subset of (TOP-REAL 2) st b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 <= b1 } holds
b2 is closed
proof end;

theorem Th10: :: JORDAN6:10
for b1 being real number
for b2 being Subset of (TOP-REAL 2) st b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 = b1 } holds
b2 is closed
proof end;

theorem Th11: :: JORDAN6:11
for b1 being Nat
for b2 being Subset of (TOP-REAL b1)
for b3, b4 being Point of (TOP-REAL b1) st b2 is_an_arc_of b3,b4 holds
b2 is connected
proof end;

theorem Th12: :: JORDAN6:12
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 holds
b1 is closed
proof end;

theorem Th13: :: JORDAN6:13
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 holds
ex b4 being Point of (TOP-REAL 2) st
( b4 in b1 & b4 `1 = ((b2 `1 ) + (b3 `1 )) / 2 )
proof end;

theorem Th14: :: JORDAN6:14
for b1, b2 being Subset of (TOP-REAL 2)
for b3, b4 being Point of (TOP-REAL 2) st b1 is_an_arc_of b3,b4 & b2 = { b5 where B is Point of (TOP-REAL 2) : b5 `1 = ((b3 `1 ) + (b4 `1 )) / 2 } holds
( b1 meets b2 & b1 /\ b2 is closed )
proof end;

theorem Th15: :: JORDAN6:15
for b1, b2 being Subset of (TOP-REAL 2)
for b3, b4 being Point of (TOP-REAL 2) st b1 is_an_arc_of b3,b4 & b2 = { b5 where B is Point of (TOP-REAL 2) : b5 `2 = ((b3 `2 ) + (b4 `2 )) / 2 } holds
( b1 meets b2 & b1 /\ b2 is closed )
proof end;

definition
let c1 be Subset of (TOP-REAL 2);
let c2, c3 be Point of (TOP-REAL 2);
func x_Middle c1,c2,c3 -> Point of (TOP-REAL 2) means :Def1: :: JORDAN6:def 1
for b1 being Subset of (TOP-REAL 2) st b1 = { b2 where B is Point of (TOP-REAL 2) : b2 `1 = ((a2 `1 ) + (a3 `1 )) / 2 } holds
a4 = First_Point a1,a2,a3,b1;
existence
ex b1 being Point of (TOP-REAL 2) st
for b2 being Subset of (TOP-REAL 2) st b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `1 = ((c2 `1 ) + (c3 `1 )) / 2 } holds
b1 = First_Point c1,c2,c3,b2
proof end;
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st ( for b3 being Subset of (TOP-REAL 2) st b3 = { b4 where B is Point of (TOP-REAL 2) : b4 `1 = ((c2 `1 ) + (c3 `1 )) / 2 } holds
b1 = First_Point c1,c2,c3,b3 ) & ( for b3 being Subset of (TOP-REAL 2) st b3 = { b4 where B is Point of (TOP-REAL 2) : b4 `1 = ((c2 `1 ) + (c3 `1 )) / 2 } holds
b2 = First_Point c1,c2,c3,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines x_Middle JORDAN6:def 1 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2) holds
( b4 = x_Middle b1,b2,b3 iff for b5 being Subset of (TOP-REAL 2) st b5 = { b6 where B is Point of (TOP-REAL 2) : b6 `1 = ((b2 `1 ) + (b3 `1 )) / 2 } holds
b4 = First_Point b1,b2,b3,b5 );

definition
let c1 be Subset of (TOP-REAL 2);
let c2, c3 be Point of (TOP-REAL 2);
func y_Middle c1,c2,c3 -> Point of (TOP-REAL 2) means :Def2: :: JORDAN6:def 2
for b1 being Subset of (TOP-REAL 2) st b1 = { b2 where B is Point of (TOP-REAL 2) : b2 `2 = ((a2 `2 ) + (a3 `2 )) / 2 } holds
a4 = First_Point a1,a2,a3,b1;
existence
ex b1 being Point of (TOP-REAL 2) st
for b2 being Subset of (TOP-REAL 2) st b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 = ((c2 `2 ) + (c3 `2 )) / 2 } holds
b1 = First_Point c1,c2,c3,b2
proof end;
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st ( for b3 being Subset of (TOP-REAL 2) st b3 = { b4 where B is Point of (TOP-REAL 2) : b4 `2 = ((c2 `2 ) + (c3 `2 )) / 2 } holds
b1 = First_Point c1,c2,c3,b3 ) & ( for b3 being Subset of (TOP-REAL 2) st b3 = { b4 where B is Point of (TOP-REAL 2) : b4 `2 = ((c2 `2 ) + (c3 `2 )) / 2 } holds
b2 = First_Point c1,c2,c3,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines y_Middle JORDAN6:def 2 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2) holds
( b4 = y_Middle b1,b2,b3 iff for b5 being Subset of (TOP-REAL 2) st b5 = { b6 where B is Point of (TOP-REAL 2) : b6 `2 = ((b2 `2 ) + (b3 `2 )) / 2 } holds
b4 = First_Point b1,b2,b3,b5 );

theorem Th16: :: JORDAN6:16
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 holds
( x_Middle b1,b2,b3 in b1 & y_Middle b1,b2,b3 in b1 )
proof end;

theorem Th17: :: JORDAN6:17
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 holds
( b2 = x_Middle b1,b2,b3 iff b2 `1 = b3 `1 )
proof end;

theorem Th18: :: JORDAN6:18
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 holds
( b2 = y_Middle b1,b2,b3 iff b2 `2 = b3 `2 )
proof end;

theorem Th19: :: JORDAN6:19
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 & LE b4,b5,b1,b2,b3 holds
LE b5,b4,b1,b3,b2
proof end;

definition
let c1 be Subset of (TOP-REAL 2);
let c2, c3, c4 be Point of (TOP-REAL 2);
func L_Segment c1,c2,c3,c4 -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 3
{ b1 where B is Point of (TOP-REAL 2) : LE b1,a4,a1,a2,a3 } ;
coherence
{ b1 where B is Point of (TOP-REAL 2) : LE b1,c4,c1,c2,c3 } is Subset of (TOP-REAL 2)
proof end;
end;

:: deftheorem Def3 defines L_Segment JORDAN6:def 3 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2) holds L_Segment b1,b2,b3,b4 = { b5 where B is Point of (TOP-REAL 2) : LE b5,b4,b1,b2,b3 } ;

definition
let c1 be Subset of (TOP-REAL 2);
let c2, c3, c4 be Point of (TOP-REAL 2);
func R_Segment c1,c2,c3,c4 -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 4
{ b1 where B is Point of (TOP-REAL 2) : LE a4,b1,a1,a2,a3 } ;
coherence
{ b1 where B is Point of (TOP-REAL 2) : LE c4,b1,c1,c2,c3 } is Subset of (TOP-REAL 2)
proof end;
end;

:: deftheorem Def4 defines R_Segment JORDAN6:def 4 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2) holds R_Segment b1,b2,b3,b4 = { b5 where B is Point of (TOP-REAL 2) : LE b4,b5,b1,b2,b3 } ;

theorem Th20: :: JORDAN6:20
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2) holds L_Segment b1,b2,b3,b4 c= b1
proof end;

theorem Th21: :: JORDAN6:21
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2) holds R_Segment b1,b2,b3,b4 c= b1
proof end;

theorem Th22: :: JORDAN6:22
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 holds
L_Segment b1,b2,b3,b2 = {b2}
proof end;

theorem Th23: :: JORDAN6:23
canceled;

theorem Th24: :: JORDAN6:24
canceled;

theorem Th25: :: JORDAN6:25
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 holds
L_Segment b1,b2,b3,b3 = b1
proof end;

theorem Th26: :: JORDAN6:26
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 holds
R_Segment b1,b2,b3,b3 = {b3}
proof end;

theorem Th27: :: JORDAN6:27
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 holds
R_Segment b1,b2,b3,b2 = b1
proof end;

theorem Th28: :: JORDAN6:28
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 & b4 in b1 holds
R_Segment b1,b2,b3,b4 = L_Segment b1,b3,b2,b4
proof end;

definition
let c1 be Subset of (TOP-REAL 2);
let c2, c3, c4, c5 be Point of (TOP-REAL 2);
func Segment c1,c2,c3,c4,c5 -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 5
(R_Segment a1,a2,a3,a4) /\ (L_Segment a1,a2,a3,a5);
correctness
coherence
(R_Segment c1,c2,c3,c4) /\ (L_Segment c1,c2,c3,c5) is Subset of (TOP-REAL 2);
;
end;

:: deftheorem Def5 defines Segment JORDAN6:def 5 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4, b5 being Point of (TOP-REAL 2) holds Segment b1,b2,b3,b4,b5 = (R_Segment b1,b2,b3,b4) /\ (L_Segment b1,b2,b3,b5);

theorem Th29: :: JORDAN6:29
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4, b5 being Point of (TOP-REAL 2) holds Segment b1,b2,b3,b4,b5 = { b6 where B is Point of (TOP-REAL 2) : ( LE b4,b6,b1,b2,b3 & LE b6,b5,b1,b2,b3 ) }
proof end;

theorem Th30: :: JORDAN6:30
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 holds
( LE b4,b5,b1,b2,b3 iff LE b5,b4,b1,b3,b2 )
proof end;

theorem Th31: :: JORDAN6:31
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 & b4 in b1 holds
L_Segment b1,b2,b3,b4 = R_Segment b1,b3,b2,b4
proof end;

theorem Th32: :: JORDAN6:32
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 & b4 in b1 & b5 in b1 holds
Segment b1,b2,b3,b4,b5 = Segment b1,b3,b2,b5,b4
proof end;

definition
let c1 be real number ;
func Vertical_Line c1 -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 6
{ b1 where B is Point of (TOP-REAL 2) : b1 `1 = a1 } ;
correctness
coherence
{ b1 where B is Point of (TOP-REAL 2) : b1 `1 = c1 } is Subset of (TOP-REAL 2);
proof end;
func Horizontal_Line c1 -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 7
{ b1 where B is Point of (TOP-REAL 2) : b1 `2 = a1 } ;
correctness
coherence
{ b1 where B is Point of (TOP-REAL 2) : b1 `2 = c1 } is Subset of (TOP-REAL 2);
proof end;
end;

:: deftheorem Def6 defines Vertical_Line JORDAN6:def 6 :
for b1 being real number holds Vertical_Line b1 = { b2 where B is Point of (TOP-REAL 2) : b2 `1 = b1 } ;

:: deftheorem Def7 defines Horizontal_Line JORDAN6:def 7 :
for b1 being real number holds Horizontal_Line b1 = { b2 where B is Point of (TOP-REAL 2) : b2 `2 = b1 } ;

theorem Th33: :: JORDAN6:33
for b1 being real number holds
( Vertical_Line b1 is closed & Horizontal_Line b1 is closed ) by Th7, Th10;

theorem Th34: :: JORDAN6:34
for b1 being real number
for b2 being Point of (TOP-REAL 2) holds
( b2 in Vertical_Line b1 iff b2 `1 = b1 )
proof end;

theorem Th35: :: JORDAN6:35
for b1 being real number
for b2 being Point of (TOP-REAL 2) holds
( b2 in Horizontal_Line b1 iff b2 `2 = b1 )
proof end;

theorem Th36: :: JORDAN6:36
canceled;

theorem Th37: :: JORDAN6:37
canceled;

theorem Th38: :: JORDAN6:38
canceled;

theorem Th39: :: JORDAN6:39
canceled;

theorem Th40: :: JORDAN6:40
for b1 being Subset of (TOP-REAL 2) st b1 is_simple_closed_curve holds
ex b2, b3 being non empty Subset of (TOP-REAL 2) st
( b2 is_an_arc_of W-min b1, E-max b1 & b3 is_an_arc_of E-max b1, W-min b1 & b2 /\ b3 = {(W-min b1),(E-max b1)} & b2 \/ b3 = b1 & (First_Point b2,(W-min b1),(E-max b1),(Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) `2 > (Last_Point b3,(E-max b1),(W-min b1),(Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) `2 )
proof end;

theorem Th41: :: JORDAN6:41
for b1 being Subset of I[01] st b1 = the carrier of I[01] \ {0,1} holds
b1 is open
proof end;

Lemma26: for b1, b2 being real number holds ].b1,b2.[ misses {b1,b2}
by RCOMP_1:46;

Lemma27: for b1, b2, b3 being real number holds
( b3 in ].b1,b2.[ iff ( b1 < b3 & b3 < b2 ) )
by RCOMP_1:47;

theorem Th42: :: JORDAN6:42
canceled;

theorem Th43: :: JORDAN6:43
canceled;

theorem Th44: :: JORDAN6:44
canceled;

theorem Th45: :: JORDAN6:45
canceled;

theorem Th46: :: JORDAN6:46
for b1 being Subset of R^1
for b2, b3 being real number st b1 = ].b2,b3.[ holds
b1 is open
proof end;

theorem Th47: :: JORDAN6:47
for b1 being TopSpace
for b2, b3 being Subset of b1
for b4 being Subset of (b1 | b3) st b2 = b4 & b2 c= b3 holds
b1 | b2 = (b1 | b3) | b4
proof end;

theorem Th48: :: JORDAN6:48
for b1 being Subset of I[01] st b1 = the carrier of I[01] \ {0,1} holds
( b1 <> {} & b1 is connected )
proof end;

theorem Th49: :: JORDAN6:49
for b1 being Nat
for b2 being Subset of (TOP-REAL b1)
for b3, b4 being Point of (TOP-REAL b1) st b2 is_an_arc_of b3,b4 holds
b3 <> b4
proof end;

theorem Th50: :: JORDAN6:50
for b1 being Nat
for b2 being Subset of (TOP-REAL b1)
for b3 being Subset of ((TOP-REAL b1) | b2)
for b4, b5 being Point of (TOP-REAL b1) st b2 is_an_arc_of b4,b5 & b3 = b2 \ {b4,b5} holds
b3 is open
proof end;

theorem Th51: :: JORDAN6:51
canceled;

theorem Th52: :: JORDAN6:52
for b1 being Nat
for b2, b3, b4 being Subset of (TOP-REAL b1)
for b5 being Subset of ((TOP-REAL b1) | b2)
for b6, b7 being Point of (TOP-REAL b1) st b6 in b2 & b7 in b2 & b3 is_an_arc_of b6,b7 & b4 is_an_arc_of b6,b7 & b3 \/ b4 = b2 & b3 /\ b4 = {b6,b7} & b5 = b3 \ {b6,b7} holds
b5 is open
proof end;

theorem Th53: :: JORDAN6:53
for b1 being Nat
for b2 being Subset of (TOP-REAL b1)
for b3 being Subset of ((TOP-REAL b1) | b2)
for b4, b5 being Point of (TOP-REAL b1) st b2 is_an_arc_of b4,b5 & b3 = b2 \ {b4,b5} holds
b3 is connected
proof end;

theorem Th54: :: JORDAN6:54
for b1 being TopSpace
for b2, b3 being Subset of b1
for b4 being Subset of (b1 | b2)
for b5 being Subset of (b1 | b3) st b2 c= b3 & b5 = b4 & b4 is connected holds
b5 is connected
proof end;

theorem Th55: :: JORDAN6:55
for b1 being Nat
for b2 being Subset of (TOP-REAL b1)
for b3, b4 being Point of (TOP-REAL b1) st b2 is_an_arc_of b3,b4 holds
ex b5 being Point of (TOP-REAL b1) st
( b5 in b2 & b5 <> b3 & b5 <> b4 )
proof end;

theorem Th56: :: JORDAN6:56
for b1 being Nat
for b2 being Subset of (TOP-REAL b1)
for b3, b4 being Point of (TOP-REAL b1) st b2 is_an_arc_of b3,b4 holds
b2 \ {b3,b4} <> {}
proof end;

theorem Th57: :: JORDAN6:57
for b1 being Nat
for b2, b3 being Subset of (TOP-REAL b1)
for b4 being Subset of ((TOP-REAL b1) | b3)
for b5, b6 being Point of (TOP-REAL b1) st b2 is_an_arc_of b5,b6 & b2 c= b3 & b4 = b2 \ {b5,b6} holds
b4 is connected
proof end;

theorem Th58: :: JORDAN6:58
for b1, b2, b3 being non empty TopSpace
for b4 being non empty Subset of b2
for b5 being Subset of b2
for b6 being Function of b1,(b2 | b4)
for b7 being Function of (b2 | b5),b3 st b4 c= b5 & b6 is continuous & b7 is continuous holds
ex b8 being Function of b1,b3 st
( b8 = b7 * b6 & b8 is continuous )
proof end;

theorem Th59: :: JORDAN6:59
for b1 being Nat
for b2, b3 being Subset of (TOP-REAL b1)
for b4, b5 being Point of (TOP-REAL b1) st b2 is_an_arc_of b4,b5 & b3 is_an_arc_of b4,b5 & b2 c= b3 holds
b2 = b3
proof end;

theorem Th60: :: JORDAN6:60
for b1 being Subset of (TOP-REAL 2)
for b2 being Subset of ((TOP-REAL 2) | b1)
for b3, b4 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & b3 in b1 & b4 in b1 & b3 <> b4 & b2 = b1 \ {b3,b4} holds
not b2 is connected
proof end;

theorem Th61: :: JORDAN6:61
for b1, b2, b3, b4, b5 being Subset of (TOP-REAL 2)
for b6, b7 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & b2 is_an_arc_of b6,b7 & b3 is_an_arc_of b6,b7 & b2 \/ b3 = b1 & b4 is_an_arc_of b6,b7 & b5 is_an_arc_of b6,b7 & b4 \/ b5 = b1 & not ( b2 = b4 & b3 = b5 ) holds
( b2 = b5 & b3 = b4 )
proof end;

registration
cluster -> real Element of the carrier of R^1 ;
coherence
for b1 being Element of R^1 holds b1 is real by TOPMETR:24, XREAL_0:def 1;
end;

Lemma39: for b1 being Function of I[01] ,R^1
for b2, b3, b4 being real number st b1 is continuous & b1 . 0[01] < b4 & b4 < b1 . 1[01] & b2 = b1 . 0 & b3 = b1 . 1 holds
ex b5 being Real st
( 0 < b5 & b5 < 1 & b1 . b5 = b4 )
proof end;

theorem Th62: :: JORDAN6:62
canceled;

theorem Th63: :: JORDAN6:63
canceled;

theorem Th64: :: JORDAN6:64
for b1 being Subset of (TOP-REAL 2)
for b2 being real number
for b3, b4 being Point of (TOP-REAL 2) st b3 `1 <= b2 & b2 <= b4 `1 & b1 is_an_arc_of b3,b4 holds
( b1 meets Vertical_Line b2 & b1 /\ (Vertical_Line b2) is closed )
proof end;

E41: now
let c1 be Simple_closed_curve;
let c2, c3 be non empty Subset of (TOP-REAL 2);
assume E42: ( ex b1 being non empty Subset of (TOP-REAL 2) st
( c2 is_an_arc_of W-min c1, E-max c1 & b1 is_an_arc_of E-max c1, W-min c1 & c2 /\ b1 = {(W-min c1),(E-max c1)} & c2 \/ b1 = c1 & (First_Point c2,(W-min c1),(E-max c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 > (Last_Point b1,(E-max c1),(W-min c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 ) & ex b1 being non empty Subset of (TOP-REAL 2) st
( c3 is_an_arc_of W-min c1, E-max c1 & b1 is_an_arc_of E-max c1, W-min c1 & c3 /\ b1 = {(W-min c1),(E-max c1)} & c3 \/ b1 = c1 & (First_Point c3,(W-min c1),(E-max c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 > (Last_Point b1,(E-max c1),(W-min c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 ) ) ;
then consider c4 being non empty Subset of (TOP-REAL 2) such that
E43: ( c2 is_an_arc_of W-min c1, E-max c1 & c4 is_an_arc_of E-max c1, W-min c1 & c2 /\ c4 = {(W-min c1),(E-max c1)} & c2 \/ c4 = c1 & (First_Point c2,(W-min c1),(E-max c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 > (Last_Point c4,(E-max c1),(W-min c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 ) ;
E44: c4 is_an_arc_of W-min c1, E-max c1 by E43, JORDAN5B:14;
consider c5 being non empty Subset of (TOP-REAL 2) such that
E45: ( c3 is_an_arc_of W-min c1, E-max c1 & c5 is_an_arc_of E-max c1, W-min c1 & c3 /\ c5 = {(W-min c1),(E-max c1)} & c3 \/ c5 = c1 & (First_Point c3,(W-min c1),(E-max c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 > (Last_Point c5,(E-max c1),(W-min c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 ) by E42;
E46: c5 is_an_arc_of W-min c1, E-max c1 by E45, JORDAN5B:14;
now
assume E47: ( c2 = c5 & c4 = c3 ) ;
E48: (W-min c1) `1 = W-bound c1 by PSCOMP_1:84;
E49: (E-max c1) `1 = E-bound c1 by PSCOMP_1:104;
then (W-min c1) `1 < (E-max c1) `1 by E48, TOPREAL5:23;
then E50: ( (W-min c1) `1 <= ((W-bound c1) + (E-bound c1)) / 2 & ((W-bound c1) + (E-bound c1)) / 2 <= (E-max c1) `1 ) by E48, E49, TOPREAL3:3;
then ( c4 meets Vertical_Line (((W-bound c1) + (E-bound c1)) / 2) & c4 /\ (Vertical_Line (((W-bound c1) + (E-bound c1)) / 2)) is closed ) by E44, Th64;
then E51: (First_Point c2,(W-min c1),(E-max c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 > (First_Point c4,(W-min c1),(E-max c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 by E43, JORDAN5C:18;
( c5 meets Vertical_Line (((W-bound c1) + (E-bound c1)) / 2) & c5 /\ (Vertical_Line (((W-bound c1) + (E-bound c1)) / 2)) is closed ) by E46, E50, Th64;
hence contradiction by E45, E47, E51, JORDAN5C:18;
end;
hence c2 = c3 by E43, E44, E45, E46, Th61;
end;

definition
let c1 be Subset of (TOP-REAL 2);
assume E42: c1 is_simple_closed_curve ;
func Upper_Arc c1 -> non empty Subset of (TOP-REAL 2) means :Def8: :: JORDAN6:def 8
( a2 is_an_arc_of W-min a1, E-max a1 & ex b1 being non empty Subset of (TOP-REAL 2) st
( b1 is_an_arc_of E-max a1, W-min a1 & a2 /\ b1 = {(W-min a1),(E-max a1)} & a2 \/ b1 = a1 & (First_Point a2,(W-min a1),(E-max a1),(Vertical_Line (((W-bound a1) + (E-bound a1)) / 2))) `2 > (Last_Point b1,(E-max a1),(W-min a1),(Vertical_Line (((W-bound a1) + (E-bound a1)) / 2))) `2 ) );
existence
ex b1 being non empty Subset of (TOP-REAL 2) st
( b1 is_an_arc_of W-min c1, E-max c1 & ex b2 being non empty Subset of (TOP-REAL 2) st
( b2 is_an_arc_of E-max c1, W-min c1 & b1 /\ b2 = {(W-min c1),(E-max c1)} & b1 \/ b2 = c1 & (First_Point b1,(W-min c1),(E-max c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 > (Last_Point b2,(E-max c1),(W-min c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 ) )
proof end;
uniqueness
for b1, b2 being non empty Subset of (TOP-REAL 2) st b1 is_an_arc_of W-min c1, E-max c1 & ex b3 being non empty Subset of (TOP-REAL 2) st
( b3 is_an_arc_of E-max c1, W-min c1 & b1 /\ b3 = {(W-min c1),(E-max c1)} & b1 \/ b3 = c1 & (First_Point b1,(W-min c1),(E-max c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 > (Last_Point b3,(E-max c1),(W-min c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 ) & b2 is_an_arc_of W-min c1, E-max c1 & ex b3 being non empty Subset of (TOP-REAL 2) st
( b3 is_an_arc_of E-max c1, W-min c1 & b2 /\ b3 = {(W-min c1),(E-max c1)} & b2 \/ b3 = c1 & (First_Point b2,(W-min c1),(E-max c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 > (Last_Point b3,(E-max c1),(W-min c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 ) holds
b1 = b2 by E42, Lemma41;
end;

:: deftheorem Def8 defines Upper_Arc JORDAN6:def 8 :
for b1 being Subset of (TOP-REAL 2) st b1 is_simple_closed_curve holds
for b2 being non empty Subset of (TOP-REAL 2) holds
( b2 = Upper_Arc b1 iff ( b2 is_an_arc_of W-min b1, E-max b1 & ex b3 being non empty Subset of (TOP-REAL 2) st
( b3 is_an_arc_of E-max b1, W-min b1 & b2 /\ b3 = {(W-min b1),(E-max b1)} & b2 \/ b3 = b1 & (First_Point b2,(W-min b1),(E-max b1),(Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) `2 > (Last_Point b3,(E-max b1),(W-min b1),(Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) `2 ) ) );

definition
let c1 be Subset of (TOP-REAL 2);
assume E43: c1 is_simple_closed_curve ;
then E44: Upper_Arc c1 is_an_arc_of W-min c1, E-max c1 by Def8;
func Lower_Arc c1 -> non empty Subset of (TOP-REAL 2) means :Def9: :: JORDAN6:def 9
( a2 is_an_arc_of E-max a1, W-min a1 & (Upper_Arc a1) /\ a2 = {(W-min a1),(E-max a1)} & (Upper_Arc a1) \/ a2 = a1 & (First_Point (Upper_Arc a1),(W-min a1),(E-max a1),(Vertical_Line (((W-bound a1) + (E-bound a1)) / 2))) `2 > (Last_Point a2,(E-max a1),(W-min a1),(Vertical_Line (((W-bound a1) + (E-bound a1)) / 2))) `2 );
existence
ex b1 being non empty Subset of (TOP-REAL 2) st
( b1 is_an_arc_of E-max c1, W-min c1 & (Upper_Arc c1) /\ b1 = {(W-min c1),(E-max c1)} & (Upper_Arc c1) \/ b1 = c1 & (First_Point (Upper_Arc c1),(W-min c1),(E-max c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 > (Last_Point b1,(E-max c1),(W-min c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 ) by E43, Def8;
uniqueness
for b1, b2 being non empty Subset of (TOP-REAL 2) st b1 is_an_arc_of E-max c1, W-min c1 & (Upper_Arc c1) /\ b1 = {(W-min c1),(E-max c1)} & (Upper_Arc c1) \/ b1 = c1 & (First_Point (Upper_Arc c1),(W-min c1),(E-max c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 > (Last_Point b1,(E-max c1),(W-min c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 & b2 is_an_arc_of E-max c1, W-min c1 & (Upper_Arc c1) /\ b2 = {(W-min c1),(E-max c1)} & (Upper_Arc c1) \/ b2 = c1 & (First_Point (Upper_Arc c1),(W-min c1),(E-max c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 > (Last_Point b2,(E-max c1),(W-min c1),(Vertical_Line (((W-bound c1) + (E-bound c1)) / 2))) `2 holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Lower_Arc JORDAN6:def 9 :
for b1 being Subset of (TOP-REAL 2) st b1 is_simple_closed_curve holds
for b2 being non empty Subset of (TOP-REAL 2) holds
( b2 = Lower_Arc b1 iff ( b2 is_an_arc_of E-max b1, W-min b1 & (Upper_Arc b1) /\ b2 = {(W-min b1),(E-max b1)} & (Upper_Arc b1) \/ b2 = b1 & (First_Point (Upper_Arc b1),(W-min b1),(E-max b1),(Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) `2 > (Last_Point b2,(E-max b1),(W-min b1),(Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) `2 ) );

theorem Th65: :: JORDAN6:65
for b1 being Subset of (TOP-REAL 2) st b1 is_simple_closed_curve holds
( Upper_Arc b1 is_an_arc_of W-min b1, E-max b1 & Upper_Arc b1 is_an_arc_of E-max b1, W-min b1 & Lower_Arc b1 is_an_arc_of E-max b1, W-min b1 & Lower_Arc b1 is_an_arc_of W-min b1, E-max b1 & (Upper_Arc b1) /\ (Lower_Arc b1) = {(W-min b1),(E-max b1)} & (Upper_Arc b1) \/ (Lower_Arc b1) = b1 & (First_Point (Upper_Arc b1),(W-min b1),(E-max b1),(Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) `2 > (Last_Point (Lower_Arc b1),(E-max b1),(W-min b1),(Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) `2 )
proof end;

theorem Th66: :: JORDAN6:66
for b1 being Subset of (TOP-REAL 2) st b1 is_simple_closed_curve holds
( Lower_Arc b1 = (b1 \ (Upper_Arc b1)) \/ {(W-min b1),(E-max b1)} & Upper_Arc b1 = (b1 \ (Lower_Arc b1)) \/ {(W-min b1),(E-max b1)} )
proof end;

theorem Th67: :: JORDAN6:67
for b1 being Subset of (TOP-REAL 2)
for b2 being Subset of ((TOP-REAL 2) | b1) st b1 is_simple_closed_curve & (Upper_Arc b1) /\ b2 = {(W-min b1),(E-max b1)} & (Upper_Arc b1) \/ b2 = b1 holds
b2 = Lower_Arc b1
proof end;

theorem Th68: :: JORDAN6:68
for b1 being Subset of (TOP-REAL 2)
for b2 being Subset of ((TOP-REAL 2) | b1) st b1 is_simple_closed_curve & b2 /\ (Lower_Arc b1) = {(W-min b1),(E-max b1)} & b2 \/ (Lower_Arc b1) = b1 holds
b2 = Upper_Arc b1
proof end;

theorem Th69: :: JORDAN6:69
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 & LE b4,b2,b1,b2,b3 holds
b4 = b2
proof end;

theorem Th70: :: JORDAN6:70
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 & LE b3,b4,b1,b2,b3 holds
b4 = b3
proof end;

definition
let c1 be Subset of (TOP-REAL 2);
let c2, c3 be Point of (TOP-REAL 2);
pred LE c2,c3,c1 means :Def10: :: JORDAN6:def 10
( ( a2 in Upper_Arc a1 & a3 in Lower_Arc a1 & not a3 = W-min a1 ) or ( a2 in Upper_Arc a1 & a3 in Upper_Arc a1 & LE a2,a3, Upper_Arc a1, W-min a1, E-max a1 ) or ( a2 in Lower_Arc a1 & a3 in Lower_Arc a1 & not a3 = W-min a1 & LE a2,a3, Lower_Arc a1, E-max a1, W-min a1 ) );
end;

:: deftheorem Def10 defines LE JORDAN6:def 10 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) holds
( LE b2,b3,b1 iff ( ( b2 in Upper_Arc b1 & b3 in Lower_Arc b1 & not b3 = W-min b1 ) or ( b2 in Upper_Arc b1 & b3 in Upper_Arc b1 & LE b2,b3, Upper_Arc b1, W-min b1, E-max b1 ) or ( b2 in Lower_Arc b1 & b3 in Lower_Arc b1 & not b3 = W-min b1 & LE b2,b3, Lower_Arc b1, E-max b1, W-min b1 ) ) );

theorem Th71: :: JORDAN6:71
for b1 being Subset of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & b2 in b1 holds
LE b2,b2,b1
proof end;

theorem Th72: :: JORDAN6:72
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & LE b2,b3,b1 & LE b3,b2,b1 holds
b2 = b3
proof end;

theorem Th73: :: JORDAN6:73
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & LE b2,b3,b1 & LE b3,b4,b1 holds
LE b2,b4,b1
proof end;