:: JORDAN17 semantic presentation

theorem Th1: :: JORDAN17:1
for b1 being Nat
for b2, b3, b4 being Point of (TOP-REAL b1)
for b5 being Subset of (TOP-REAL b1) st b2 in b5 & b5 is_an_arc_of b3,b4 holds
ex b6 being Function of I[01] ,((TOP-REAL b1) | b5)ex b7 being Real st
( b6 is_homeomorphism & b6 . 0 = b3 & b6 . 1 = b4 & 0 <= b7 & b7 <= 1 & b6 . b7 = b2 )
proof end;

theorem Th2: :: JORDAN17:2
for b1 being Simple_closed_curve holds LE W-min b1, E-max b1,b1
proof end;

theorem Th3: :: JORDAN17:3
for b1 being Simple_closed_curve
for b2 being Point of (TOP-REAL 2) st LE b2, E-max b1,b1 holds
b2 in Upper_Arc b1
proof end;

theorem Th4: :: JORDAN17:4
for b1 being Simple_closed_curve
for b2 being Point of (TOP-REAL 2) st LE E-max b1,b2,b1 holds
b2 in Lower_Arc b1
proof end;

theorem Th5: :: JORDAN17:5
for b1 being Simple_closed_curve
for b2 being Point of (TOP-REAL 2) st LE b2, W-min b1,b1 holds
b2 in Lower_Arc b1
proof end;

theorem Th6: :: JORDAN17:6
for b1, b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Subset of (TOP-REAL 2) st b1 <> b2 & b5 is_an_arc_of b3,b4 & LE b1,b2,b5,b3,b4 holds
ex b6 being Point of (TOP-REAL 2) st
( b1 <> b6 & b2 <> b6 & LE b1,b6,b5,b3,b4 & LE b6,b2,b5,b3,b4 )
proof end;

theorem Th7: :: JORDAN17:7
for b1 being Simple_closed_curve
for b2 being Point of (TOP-REAL 2) st b2 in b1 holds
ex b3 being Point of (TOP-REAL 2) st
( b2 <> b3 & LE b2,b3,b1 )
proof end;

theorem Th8: :: JORDAN17:8
for b1 being Simple_closed_curve
for b2, b3 being Point of (TOP-REAL 2) st b2 <> b3 & LE b2,b3,b1 holds
ex b4 being Point of (TOP-REAL 2) st
( b4 <> b2 & b4 <> b3 & LE b2,b4,b1 & LE b4,b3,b1 )
proof end;

definition
let c1 be Subset of (TOP-REAL 2);
let c2, c3, c4, c5 be Point of (TOP-REAL 2);
pred c2,c3,c4,c5 are_in_this_order_on c1 means :Def1: :: JORDAN17:def 1
( ( LE a2,a3,a1 & LE a3,a4,a1 & LE a4,a5,a1 ) or ( LE a3,a4,a1 & LE a4,a5,a1 & LE a5,a2,a1 ) or ( LE a4,a5,a1 & LE a5,a2,a1 & LE a2,a3,a1 ) or ( LE a5,a2,a1 & LE a2,a3,a1 & LE a3,a4,a1 ) );
end;

:: deftheorem Def1 defines are_in_this_order_on JORDAN17:def 1 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4, b5 being Point of (TOP-REAL 2) holds
( b2,b3,b4,b5 are_in_this_order_on b1 iff ( ( LE b2,b3,b1 & LE b3,b4,b1 & LE b4,b5,b1 ) or ( LE b3,b4,b1 & LE b4,b5,b1 & LE b5,b2,b1 ) or ( LE b4,b5,b1 & LE b5,b2,b1 & LE b2,b3,b1 ) or ( LE b5,b2,b1 & LE b2,b3,b1 & LE b3,b4,b1 ) ) );

theorem Th9: :: JORDAN17:9
for b1 being Simple_closed_curve
for b2 being Point of (TOP-REAL 2) st b2 in b1 holds
b2,b2,b2,b2 are_in_this_order_on b1
proof end;

theorem Th10: :: JORDAN17:10
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2,b3,b4,b5 are_in_this_order_on b1 holds
b3,b4,b5,b2 are_in_this_order_on b1
proof end;

theorem Th11: :: JORDAN17:11
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2,b3,b4,b5 are_in_this_order_on b1 holds
b4,b5,b2,b3 are_in_this_order_on b1
proof end;

theorem Th12: :: JORDAN17:12
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2,b3,b4,b5 are_in_this_order_on b1 holds
b5,b2,b3,b4 are_in_this_order_on b1
proof end;

theorem Th13: :: JORDAN17:13
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b2,b3,b4,b5 are_in_this_order_on b1 holds
ex b6 being Point of (TOP-REAL 2) st
( b6 <> b2 & b6 <> b3 & b2,b6,b3,b4 are_in_this_order_on b1 )
proof end;

theorem Th14: :: JORDAN17:14
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b2,b3,b4,b5 are_in_this_order_on b1 holds
ex b6 being Point of (TOP-REAL 2) st
( b6 <> b2 & b6 <> b3 & b2,b6,b3,b5 are_in_this_order_on b1 )
proof end;

theorem Th15: :: JORDAN17:15
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b4,b2,b3,b5 are_in_this_order_on b1 holds
ex b6 being Point of (TOP-REAL 2) st
( b6 <> b2 & b6 <> b3 & b4,b2,b6,b3 are_in_this_order_on b1 )
proof end;

theorem Th16: :: JORDAN17:16
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b4,b2,b3,b5 are_in_this_order_on b1 holds
ex b6 being Point of (TOP-REAL 2) st
( b6 <> b2 & b6 <> b3 & b2,b6,b3,b5 are_in_this_order_on b1 )
proof end;

theorem Th17: :: JORDAN17:17
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b4,b5,b2,b3 are_in_this_order_on b1 holds
ex b6 being Point of (TOP-REAL 2) st
( b6 <> b2 & b6 <> b3 & b4,b2,b6,b3 are_in_this_order_on b1 )
proof end;

theorem Th18: :: JORDAN17:18
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b4,b5,b2,b3 are_in_this_order_on b1 holds
ex b6 being Point of (TOP-REAL 2) st
( b6 <> b2 & b6 <> b3 & b5,b2,b6,b3 are_in_this_order_on b1 )
proof end;

theorem Th19: :: JORDAN17:19
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b3,b4,b5,b2 are_in_this_order_on b1 holds
ex b6 being Point of (TOP-REAL 2) st
( b6 <> b2 & b6 <> b3 & b3,b4,b2,b6 are_in_this_order_on b1 )
proof end;

theorem Th20: :: JORDAN17:20
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b3,b4,b5,b2 are_in_this_order_on b1 holds
ex b6 being Point of (TOP-REAL 2) st
( b6 <> b2 & b6 <> b3 & b3,b5,b2,b6 are_in_this_order_on b1 )
proof end;

theorem Th21: :: JORDAN17:21
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b2 <> b4 & b5 <> b4 & b2,b5,b3,b4 are_in_this_order_on b1 & b5,b2,b3,b4 are_in_this_order_on b1 holds
b2 = b5
proof end;

theorem Th22: :: JORDAN17:22
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b3 <> b4 & b4 <> b5 & b2,b3,b4,b5 are_in_this_order_on b1 & b4,b3,b2,b5 are_in_this_order_on b1 holds
b2 = b4
proof end;

theorem Th23: :: JORDAN17:23
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b2 <> b4 & b3 <> b5 & b2,b3,b4,b5 are_in_this_order_on b1 & b5,b3,b4,b2 are_in_this_order_on b1 holds
b2 = b5
proof end;

theorem Th24: :: JORDAN17:24
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b2 <> b4 & b5 <> b4 & b2,b5,b3,b4 are_in_this_order_on b1 & b2,b3,b5,b4 are_in_this_order_on b1 holds
b5 = b3
proof end;

theorem Th25: :: JORDAN17:25
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b3 <> b4 & b4 <> b5 & b2,b3,b4,b5 are_in_this_order_on b1 & b2,b5,b4,b3 are_in_this_order_on b1 holds
b3 = b5
proof end;

theorem Th26: :: JORDAN17:26
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 <> b3 & b2 <> b4 & b3 <> b5 & b2,b3,b4,b5 are_in_this_order_on b1 & b2,b3,b5,b4 are_in_this_order_on b1 holds
b4 = b5
proof end;

theorem Th27: :: JORDAN17:27
for b1 being Simple_closed_curve
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b2 in b1 & b3 in b1 & b4 in b1 & b5 in b1 & not b2,b3,b4,b5 are_in_this_order_on b1 & not b2,b3,b5,b4 are_in_this_order_on b1 & not b2,b4,b3,b5 are_in_this_order_on b1 & not b2,b4,b5,b3 are_in_this_order_on b1 & not b2,b5,b3,b4 are_in_this_order_on b1 holds
b2,b5,b4,b3 are_in_this_order_on b1
proof end;