:: JORDAN7 semantic presentation

E1: 2 -' 1 = 2 - 1 by BINARITH:50
.= 1 ;

Lemma2: for b1, b2, b3 being Nat st b1 -' b3 <= b2 holds
b1 <= b2 + b3
proof end;

Lemma3: for b1, b2, b3 being Nat st b2 + b3 <= b1 holds
b3 <= b1 -' b2
proof end;

theorem Th1: :: JORDAN7:1
for b1 being non empty compact Subset of (TOP-REAL 2) st b1 is_simple_closed_curve holds
( W-min b1 in Lower_Arc b1 & E-max b1 in Lower_Arc b1 & W-min b1 in Upper_Arc b1 & E-max b1 in Upper_Arc b1 )
proof end;

theorem Th2: :: JORDAN7:2
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & LE b2, W-min b1,b1 holds
b2 = W-min b1
proof end;

theorem Th3: :: JORDAN7:3
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & b2 in b1 holds
LE W-min b1,b2,b1
proof end;

definition
let c1 be non empty compact Subset of (TOP-REAL 2);
let c2, c3 be Point of (TOP-REAL 2);
func Segment c2,c3,c1 -> Subset of (TOP-REAL 2) equals :Def1: :: JORDAN7:def 1
{ b1 where B is Point of (TOP-REAL 2) : ( LE a2,b1,a1 & LE b1,a3,a1 ) } if a3 <> W-min a1
otherwise { b1 where B is Point of (TOP-REAL 2) : ( LE a2,b1,a1 or ( a2 in a1 & b1 = W-min a1 ) ) } ;
correctness
coherence
( ( c3 <> W-min c1 implies { b1 where B is Point of (TOP-REAL 2) : ( LE c2,b1,c1 & LE b1,c3,c1 ) } is Subset of (TOP-REAL 2) ) & ( not c3 <> W-min c1 implies { b1 where B is Point of (TOP-REAL 2) : ( LE c2,b1,c1 or ( c2 in c1 & b1 = W-min c1 ) ) } is Subset of (TOP-REAL 2) ) );
consistency
for b1 being Subset of (TOP-REAL 2) holds verum;
proof end;
end;

:: deftheorem Def1 defines Segment JORDAN7:def 1 :
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) holds
( ( b3 <> W-min b1 implies Segment b2,b3,b1 = { b4 where B is Point of (TOP-REAL 2) : ( LE b2,b4,b1 & LE b4,b3,b1 ) } ) & ( not b3 <> W-min b1 implies Segment b2,b3,b1 = { b4 where B is Point of (TOP-REAL 2) : ( LE b2,b4,b1 or ( b2 in b1 & b4 = W-min b1 ) ) } ) );

theorem Th4: :: JORDAN7:4
for b1 being non empty compact Subset of (TOP-REAL 2) st b1 is_simple_closed_curve holds
( Segment (W-min b1),(E-max b1),b1 = Upper_Arc b1 & Segment (E-max b1),(W-min b1),b1 = Lower_Arc b1 )
proof end;

theorem Th5: :: JORDAN7:5
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & LE b2,b3,b1 holds
( b2 in b1 & b3 in b1 )
proof end;

theorem Th6: :: JORDAN7:6
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & LE b2,b3,b1 holds
( b2 in Segment b2,b3,b1 & b3 in Segment b2,b3,b1 )
proof end;

theorem Th7: :: JORDAN7:7
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b2 in b1 & b1 is_simple_closed_curve holds
b2 in Segment b2,(W-min b1),b1
proof end;

theorem Th8: :: JORDAN7:8
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & b2 in b1 & b2 <> W-min b1 holds
Segment b2,b2,b1 = {b2}
proof end;

theorem Th9: :: JORDAN7:9
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & b2 <> W-min b1 & b3 <> W-min b1 holds
not W-min b1 in Segment b2,b3,b1
proof end;

theorem Th10: :: JORDAN7:10
for b1 being non empty compact 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 & ( not b2 = b3 or not b2 = W-min b1 ) & b2 <> b4 & ( not b3 = b4 or not b3 = W-min b1 ) holds
(Segment b2,b3,b1) /\ (Segment b3,b4,b1) = {b3}
proof end;

theorem Th11: :: JORDAN7:11
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & LE b2,b3,b1 & b2 <> W-min b1 & b3 <> W-min b1 holds
(Segment b2,b3,b1) /\ (Segment b3,(W-min b1),b1) = {b3}
proof end;

theorem Th12: :: JORDAN7:12
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & LE b2,b3,b1 & b2 <> b3 & b2 <> W-min b1 holds
(Segment b3,(W-min b1),b1) /\ (Segment (W-min b1),b2,b1) = {(W-min b1)}
proof end;

theorem Th13: :: JORDAN7:13
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b1 is_simple_closed_curve & LE b2,b3,b1 & LE b3,b4,b1 & LE b4,b5,b1 & b2 <> b3 & b3 <> b4 holds
Segment b2,b3,b1 misses Segment b4,b5,b1
proof end;

theorem Th14: :: JORDAN7:14
for b1 being non empty compact 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 & b2 <> W-min b1 & b2 <> b3 & b3 <> b4 holds
Segment b2,b3,b1 misses Segment b4,(W-min b1),b1
proof end;

theorem Th15: :: JORDAN7:15
for b1 being Nat
for b2 being non empty Subset of (TOP-REAL b1)
for b3 being Function of I[01] ,((TOP-REAL b1) | b2) st b2 <> {} & b3 is_homeomorphism holds
ex b4 being Function of I[01] ,(TOP-REAL b1) st
( b3 = b4 & b4 is continuous & b4 is one-to-one )
proof end;

theorem Th16: :: JORDAN7:16
for b1 being Nat
for b2 being non empty Subset of (TOP-REAL b1)
for b3 being Function of I[01] ,(TOP-REAL b1) st b3 is continuous & b3 is one-to-one & rng b3 = b2 holds
ex b4 being Function of I[01] ,((TOP-REAL b1) | b2) st
( b4 = b3 & b4 is_homeomorphism )
proof end;

registration
cluster increasing -> one-to-one FinSequence of REAL ;
coherence
for b1 being FinSequence of REAL st b1 is increasing holds
b1 is one-to-one
proof end;
end;

theorem Th17: :: JORDAN7:17
for b1 being FinSequence of REAL st b1 is increasing holds
b1 is one-to-one
proof end;

E19: now
let c1 be Nat;
c1 < c1 + 1 by NAT_1:38;
then c1 - 1 < (c1 + 1) - 1 by XREAL_1:11;
then ( (c1 - 1) - 1 < c1 - 1 & c1 - 1 < c1 ) by XREAL_1:11;
hence (c1 - 1) - 1 < c1 by XREAL_1:2;
end;

Lemma20: ( 0 in [.0,1.] & 1 in [.0,1.] )
by RCOMP_1:15;

theorem Th18: :: JORDAN7: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
ex b4 being Function of I[01] ,(TOP-REAL 2) st
( b4 is continuous & b4 is one-to-one & rng b4 = b1 & b4 . 0 = b2 & b4 . 1 = b3 )
proof end;

theorem Th19: :: JORDAN7:19
for b1 being non empty Subset of (TOP-REAL 2)
for b2, b3, b4, b5 being Point of (TOP-REAL 2)
for b6 being Function of I[01] ,(TOP-REAL 2)
for b7, b8 being Real st b1 is_an_arc_of b2,b3 & b6 is continuous & b6 is one-to-one & rng b6 = b1 & b6 . 0 = b2 & b6 . 1 = b3 & b6 . b7 = b4 & 0 <= b7 & b7 <= 1 & b6 . b8 = b5 & 0 <= b8 & b8 <= 1 & b7 <= b8 holds
LE b4,b5,b1,b2,b3
proof end;

theorem Th20: :: JORDAN7:20
for b1 being non empty Subset of (TOP-REAL 2)
for b2, b3, b4, b5 being Point of (TOP-REAL 2)
for b6 being Function of I[01] ,(TOP-REAL 2)
for b7, b8 being Real st b6 is continuous & b6 is one-to-one & rng b6 = b1 & b6 . 0 = b2 & b6 . 1 = b3 & b6 . b7 = b4 & 0 <= b7 & b7 <= 1 & b6 . b8 = b5 & 0 <= b8 & b8 <= 1 & LE b4,b5,b1,b2,b3 holds
b7 <= b8
proof end;

theorem Th21: :: JORDAN7:21
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2 being Real st b1 is_simple_closed_curve & b2 > 0 holds
ex b3 being FinSequence of the carrier of (TOP-REAL 2) st
( b3 . 1 = W-min b1 & b3 is one-to-one & 8 <= len b3 & rng b3 c= b1 & ( for b4 being Nat st 1 <= b4 & b4 < len b3 holds
LE b3 /. b4,b3 /. (b4 + 1),b1 ) & ( for b4 being Nat
for b5 being Subset of (Euclid 2) st 1 <= b4 & b4 < len b3 & b5 = Segment (b3 /. b4),(b3 /. (b4 + 1)),b1 holds
diameter b5 < b2 ) & ( for b4 being Subset of (Euclid 2) st b4 = Segment (b3 /. (len b3)),(b3 /. 1),b1 holds
diameter b4 < b2 ) & ( for b4 being Nat st 1 <= b4 & b4 + 1 < len b3 holds
(Segment (b3 /. b4),(b3 /. (b4 + 1)),b1) /\ (Segment (b3 /. (b4 + 1)),(b3 /. (b4 + 2)),b1) = {(b3 /. (b4 + 1))} ) & (Segment (b3 /. (len b3)),(b3 /. 1),b1) /\ (Segment (b3 /. 1),(b3 /. 2),b1) = {(b3 /. 1)} & (Segment (b3 /. ((len b3) -' 1)),(b3 /. (len b3)),b1) /\ (Segment (b3 /. (len b3)),(b3 /. 1),b1) = {(b3 /. (len b3))} & Segment (b3 /. ((len b3) -' 1)),(b3 /. (len b3)),b1 misses Segment (b3 /. 1),(b3 /. 2),b1 & ( for b4, b5 being Nat st 1 <= b4 & b4 < b5 & b5 < len b3 & not b4,b5 are_adjacent1 holds
Segment (b3 /. b4),(b3 /. (b4 + 1)),b1 misses Segment (b3 /. b5),(b3 /. (b5 + 1)),b1 ) & ( for b4 being Nat st 1 < b4 & b4 + 1 < len b3 holds
Segment (b3 /. (len b3)),(b3 /. 1),b1 misses Segment (b3 /. b4),(b3 /. (b4 + 1)),b1 ) )
proof end;