:: JORDAN20 semantic presentation

theorem Th1: :: JORDAN20:1
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
Segment b1,b2,b3,b4,b4 = {b4}
proof end;

theorem Th2: :: JORDAN20:2
for b1, b2, b3 being Point of (TOP-REAL 2)
for b4 being Real st b3 in LSeg b1,b2 & b1 `1 <= b4 & b2 `1 <= b4 holds
b3 `1 <= b4
proof end;

theorem Th3: :: JORDAN20:3
for b1, b2, b3 being Point of (TOP-REAL 2)
for b4 being Real st b3 in LSeg b1,b2 & b1 `1 >= b4 & b2 `1 >= b4 holds
b3 `1 >= b4
proof end;

theorem Th4: :: JORDAN20:4
for b1, b2, b3 being Point of (TOP-REAL 2)
for b4 being Real st b3 in LSeg b1,b2 & b1 `1 < b4 & b2 `1 < b4 holds
b3 `1 < b4
proof end;

theorem Th5: :: JORDAN20:5
for b1, b2, b3 being Point of (TOP-REAL 2)
for b4 being Real st b3 in LSeg b1,b2 & b1 `1 > b4 & b2 `1 > b4 holds
b3 `1 > b4
proof end;

theorem Th6: :: JORDAN20:6
for b1 being Nat
for b2 being S-Sequence_in_R2
for b3, b4 being Point of (TOP-REAL 2) st 1 <= b1 & b1 < len b2 & b3 in LSeg b2,b1 & b4 in LSeg b2,b1 & (b2 /. b1) `2 = (b2 /. (b1 + 1)) `2 & (b2 /. b1) `1 > (b2 /. (b1 + 1)) `1 & LE b3,b4, L~ b2,b2 /. 1,b2 /. (len b2) holds
b3 `1 >= b4 `1
proof end;

theorem Th7: :: JORDAN20:7
for b1 being Nat
for b2 being S-Sequence_in_R2
for b3, b4 being Point of (TOP-REAL 2) st 1 <= b1 & b1 < len b2 & b3 in LSeg b2,b1 & b4 in LSeg b2,b1 & (b2 /. b1) `2 = (b2 /. (b1 + 1)) `2 & (b2 /. b1) `1 < (b2 /. (b1 + 1)) `1 & LE b3,b4, L~ b2,b2 /. 1,b2 /. (len b2) holds
b3 `1 <= b4 `1
proof end;

definition
let c1 be Subset of (TOP-REAL 2);
let c2, c3, c4 be Point of (TOP-REAL 2);
let c5 be Real;
pred c4 is_Lin c1,c2,c3,c5 means :Def1: :: JORDAN20:def 1
( a1 is_an_arc_of a2,a3 & a4 in a1 & a4 `1 = a5 & ex b1 being Point of (TOP-REAL 2) st
( b1 `1 < a5 & LE b1,a4,a1,a2,a3 & ( for b2 being Point of (TOP-REAL 2) st LE b1,b2,a1,a2,a3 & LE b2,a4,a1,a2,a3 holds
b2 `1 <= a5 ) ) );
pred c4 is_Rin c1,c2,c3,c5 means :Def2: :: JORDAN20:def 2
( a1 is_an_arc_of a2,a3 & a4 in a1 & a4 `1 = a5 & ex b1 being Point of (TOP-REAL 2) st
( b1 `1 > a5 & LE b1,a4,a1,a2,a3 & ( for b2 being Point of (TOP-REAL 2) st LE b1,b2,a1,a2,a3 & LE b2,a4,a1,a2,a3 holds
b2 `1 >= a5 ) ) );
pred c4 is_Lout c1,c2,c3,c5 means :Def3: :: JORDAN20:def 3
( a1 is_an_arc_of a2,a3 & a4 in a1 & a4 `1 = a5 & ex b1 being Point of (TOP-REAL 2) st
( b1 `1 < a5 & LE a4,b1,a1,a2,a3 & ( for b2 being Point of (TOP-REAL 2) st LE b2,b1,a1,a2,a3 & LE a4,b2,a1,a2,a3 holds
b2 `1 <= a5 ) ) );
pred c4 is_Rout c1,c2,c3,c5 means :Def4: :: JORDAN20:def 4
( a1 is_an_arc_of a2,a3 & a4 in a1 & a4 `1 = a5 & ex b1 being Point of (TOP-REAL 2) st
( b1 `1 > a5 & LE a4,b1,a1,a2,a3 & ( for b2 being Point of (TOP-REAL 2) st LE b2,b1,a1,a2,a3 & LE a4,b2,a1,a2,a3 holds
b2 `1 >= a5 ) ) );
pred c4 is_OSin c1,c2,c3,c5 means :Def5: :: JORDAN20:def 5
( a1 is_an_arc_of a2,a3 & a4 in a1 & a4 `1 = a5 & ex b1 being Point of (TOP-REAL 2) st
( LE b1,a4,a1,a2,a3 & ( for b2 being Point of (TOP-REAL 2) st LE b1,b2,a1,a2,a3 & LE b2,a4,a1,a2,a3 holds
b2 `1 = a5 ) & ( for b2 being Point of (TOP-REAL 2) st LE b2,b1,a1,a2,a3 & b2 <> b1 holds
( ex b3 being Point of (TOP-REAL 2) st
( LE b2,b3,a1,a2,a3 & LE b3,b1,a1,a2,a3 & b3 `1 > a5 ) & ex b3 being Point of (TOP-REAL 2) st
( LE b2,b3,a1,a2,a3 & LE b3,b1,a1,a2,a3 & b3 `1 < a5 ) ) ) ) );
pred c4 is_OSout c1,c2,c3,c5 means :Def6: :: JORDAN20:def 6
( a1 is_an_arc_of a2,a3 & a4 in a1 & a4 `1 = a5 & ex b1 being Point of (TOP-REAL 2) st
( LE a4,b1,a1,a2,a3 & ( for b2 being Point of (TOP-REAL 2) st LE b2,b1,a1,a2,a3 & LE a4,b2,a1,a2,a3 holds
b2 `1 = a5 ) & ( for b2 being Point of (TOP-REAL 2) st LE b1,b2,a1,a2,a3 & b2 <> b1 holds
( ex b3 being Point of (TOP-REAL 2) st
( LE b3,b2,a1,a2,a3 & LE b1,b3,a1,a2,a3 & b3 `1 > a5 ) & ex b3 being Point of (TOP-REAL 2) st
( LE b3,b2,a1,a2,a3 & LE b1,b3,a1,a2,a3 & b3 `1 < a5 ) ) ) ) );
correctness
;
end;

:: deftheorem Def1 defines is_Lin JORDAN20:def 1 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Real holds
( b4 is_Lin b1,b2,b3,b5 iff ( b1 is_an_arc_of b2,b3 & b4 in b1 & b4 `1 = b5 & ex b6 being Point of (TOP-REAL 2) st
( b6 `1 < b5 & LE b6,b4,b1,b2,b3 & ( for b7 being Point of (TOP-REAL 2) st LE b6,b7,b1,b2,b3 & LE b7,b4,b1,b2,b3 holds
b7 `1 <= b5 ) ) ) );

:: deftheorem Def2 defines is_Rin JORDAN20:def 2 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Real holds
( b4 is_Rin b1,b2,b3,b5 iff ( b1 is_an_arc_of b2,b3 & b4 in b1 & b4 `1 = b5 & ex b6 being Point of (TOP-REAL 2) st
( b6 `1 > b5 & LE b6,b4,b1,b2,b3 & ( for b7 being Point of (TOP-REAL 2) st LE b6,b7,b1,b2,b3 & LE b7,b4,b1,b2,b3 holds
b7 `1 >= b5 ) ) ) );

:: deftheorem Def3 defines is_Lout JORDAN20:def 3 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Real holds
( b4 is_Lout b1,b2,b3,b5 iff ( b1 is_an_arc_of b2,b3 & b4 in b1 & b4 `1 = b5 & ex b6 being Point of (TOP-REAL 2) st
( b6 `1 < b5 & LE b4,b6,b1,b2,b3 & ( for b7 being Point of (TOP-REAL 2) st LE b7,b6,b1,b2,b3 & LE b4,b7,b1,b2,b3 holds
b7 `1 <= b5 ) ) ) );

:: deftheorem Def4 defines is_Rout JORDAN20:def 4 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Real holds
( b4 is_Rout b1,b2,b3,b5 iff ( b1 is_an_arc_of b2,b3 & b4 in b1 & b4 `1 = b5 & ex b6 being Point of (TOP-REAL 2) st
( b6 `1 > b5 & LE b4,b6,b1,b2,b3 & ( for b7 being Point of (TOP-REAL 2) st LE b7,b6,b1,b2,b3 & LE b4,b7,b1,b2,b3 holds
b7 `1 >= b5 ) ) ) );

:: deftheorem Def5 defines is_OSin JORDAN20:def 5 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Real holds
( b4 is_OSin b1,b2,b3,b5 iff ( b1 is_an_arc_of b2,b3 & b4 in b1 & b4 `1 = b5 & ex b6 being Point of (TOP-REAL 2) st
( LE b6,b4,b1,b2,b3 & ( for b7 being Point of (TOP-REAL 2) st LE b6,b7,b1,b2,b3 & LE b7,b4,b1,b2,b3 holds
b7 `1 = b5 ) & ( for b7 being Point of (TOP-REAL 2) st LE b7,b6,b1,b2,b3 & b7 <> b6 holds
( ex b8 being Point of (TOP-REAL 2) st
( LE b7,b8,b1,b2,b3 & LE b8,b6,b1,b2,b3 & b8 `1 > b5 ) & ex b8 being Point of (TOP-REAL 2) st
( LE b7,b8,b1,b2,b3 & LE b8,b6,b1,b2,b3 & b8 `1 < b5 ) ) ) ) ) );

:: deftheorem Def6 defines is_OSout JORDAN20:def 6 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Real holds
( b4 is_OSout b1,b2,b3,b5 iff ( b1 is_an_arc_of b2,b3 & b4 in b1 & b4 `1 = b5 & ex b6 being Point of (TOP-REAL 2) st
( LE b4,b6,b1,b2,b3 & ( for b7 being Point of (TOP-REAL 2) st LE b7,b6,b1,b2,b3 & LE b4,b7,b1,b2,b3 holds
b7 `1 = b5 ) & ( for b7 being Point of (TOP-REAL 2) st LE b6,b7,b1,b2,b3 & b7 <> b6 holds
( ex b8 being Point of (TOP-REAL 2) st
( LE b8,b7,b1,b2,b3 & LE b6,b8,b1,b2,b3 & b8 `1 > b5 ) & ex b8 being Point of (TOP-REAL 2) st
( LE b8,b7,b1,b2,b3 & LE b6,b8,b1,b2,b3 & b8 `1 < b5 ) ) ) ) ) );

theorem Th8: :: JORDAN20:8
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Real st b1 is_an_arc_of b2,b3 & b2 `1 <= b5 & b3 `1 >= b5 holds
ex b6 being Point of (TOP-REAL 2) st
( b6 in b1 & b6 `1 = b5 )
proof end;

theorem Th9: :: JORDAN20:9
for b1 being non empty Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Real st b1 is_an_arc_of b2,b3 & b2 `1 < b5 & b3 `1 > b5 & b4 in b1 & b4 `1 = b5 & not b4 is_Lin b1,b2,b3,b5 & not b4 is_Rin b1,b2,b3,b5 holds
b4 is_OSin b1,b2,b3,b5
proof end;

theorem Th10: :: JORDAN20:10
for b1 being non empty Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Real st b1 is_an_arc_of b2,b3 & b2 `1 < b5 & b3 `1 > b5 & b4 in b1 & b4 `1 = b5 & not b4 is_Lout b1,b2,b3,b5 & not b4 is_Rout b1,b2,b3,b5 holds
b4 is_OSout b1,b2,b3,b5
proof end;

theorem Th11: :: JORDAN20:11
for b1 being Subset of I[01]
for b2 being Real st b1 = [.0,b2.[ holds
b1 is open
proof end;

theorem Th12: :: JORDAN20:12
for b1 being Subset of I[01]
for b2 being Real st b1 = ].b2,1.] holds
b1 is open
proof end;

theorem Th13: :: JORDAN20:13
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Subset of ((TOP-REAL 2) | b1)
for b3 being Subset of I[01]
for b4 being Function of I[01] ,((TOP-REAL 2) | b1)
for b5 being Real st b5 <= 1 & b2 = { b6 where B is Point of (TOP-REAL 2) : ex b1 being Real st
( 0 <= b7 & b7 < b5 & b6 = b4 . b7 ) } & b3 = [.0,b5.[ holds
b4 .: b3 = b2
proof end;

theorem Th14: :: JORDAN20:14
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Subset of ((TOP-REAL 2) | b1)
for b3 being Subset of I[01]
for b4 being Function of I[01] ,((TOP-REAL 2) | b1)
for b5 being Real st b5 >= 0 & b2 = { b6 where B is Point of (TOP-REAL 2) : ex b1 being Real st
( b5 < b7 & b7 <= 1 & b6 = b4 . b7 ) } & b3 = ].b5,1.] holds
b4 .: b3 = b2
proof end;

theorem Th15: :: JORDAN20:15
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Subset of ((TOP-REAL 2) | b1)
for b3 being Function of I[01] ,((TOP-REAL 2) | b1)
for b4 being Real st b4 <= 1 & b3 is_homeomorphism & b2 = { b5 where B is Point of (TOP-REAL 2) : ex b1 being Real st
( 0 <= b6 & b6 < b4 & b5 = b3 . b6 ) } holds
b2 is open
proof end;

theorem Th16: :: JORDAN20:16
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Subset of ((TOP-REAL 2) | b1)
for b3 being Function of I[01] ,((TOP-REAL 2) | b1)
for b4 being Real st b4 >= 0 & b3 is_homeomorphism & b2 = { b5 where B is Point of (TOP-REAL 2) : ex b1 being Real st
( b4 < b6 & b6 <= 1 & b5 = b3 . b6 ) } holds
b2 is open
proof end;

theorem Th17: :: JORDAN20:17
for b1 being non empty TopStruct
for b2, b3 being Subset of b1
for b4, b5 being Point of b1 st b2 /\ b3 = {} & b2 \/ b3 = the carrier of b1 & b4 in b2 & b5 in b3 & b2 is open & b3 is open holds
for b6 being Function of I[01] ,b1 holds
( not b6 is continuous or not b6 . 0 = b4 or not b6 . 1 = b5 )
proof end;

theorem Th18: :: JORDAN20:18
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Subset of ((TOP-REAL 2) | b1)
for b3, b4, b5 being Point of (TOP-REAL 2) st b1 is_an_arc_of b3,b4 & b5 in b1 & b5 <> b3 & b5 <> b4 & b2 = b1 \ {b5} holds
( not b2 is connected & ( for b6 being Function of I[01] ,(((TOP-REAL 2) | b1) | b2) holds
( not b6 is continuous or not b6 . 0 = b3 or not b6 . 1 = b4 ) ) )
proof end;

theorem Th19: :: JORDAN20:19
for b1 being non empty 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 & not LE b4,b5,b1,b2,b3 holds
LE b5,b4,b1,b2,b3
proof end;

theorem Th20: :: JORDAN20:20
for b1 being non empty 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 & b2 <> b4 holds
Segment b1,b2,b3,b2,b4 is_an_arc_of b2,b4
proof end;

theorem Th21: :: JORDAN20:21
for b1 being Nat
for b2, b3 being Point of (TOP-REAL b1)
for b4, b5 being non empty Subset of (TOP-REAL b1) st b4 is_an_arc_of b2,b3 & b5 is_an_arc_of b2,b3 & b5 c= b4 holds
b5 = b4
proof end;

theorem Th22: :: JORDAN20:22
for b1 being non empty 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 & b3 <> b4 holds
Segment b1,b2,b3,b4,b3 is_an_arc_of b4,b3
proof end;

theorem Th23: :: JORDAN20:23
for b1 being non empty Subset of (TOP-REAL 2)
for b2, b3, b4, b5, b6 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 & LE b4,b5,b1,b2,b3 & LE b5,b6,b1,b2,b3 holds
(Segment b1,b2,b3,b4,b5) \/ (Segment b1,b2,b3,b5,b6) = Segment b1,b2,b3,b4,b6
proof end;

theorem Th24: :: JORDAN20:24
for b1 being non empty Subset of (TOP-REAL 2)
for b2, b3, b4, b5, b6 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 & LE b4,b5,b1,b2,b3 & LE b5,b6,b1,b2,b3 holds
(Segment b1,b2,b3,b4,b5) /\ (Segment b1,b2,b3,b5,b6) = {b5}
proof end;

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

theorem Th26: :: JORDAN20:26
canceled;

theorem Th27: :: JORDAN20:27
for b1 being non empty TopSpace
for b2, b3, b4 being Point of b1
for b5 being Path of b2,b3
for b6 being Path of b3,b4 st b5 is continuous & b6 is continuous & b5 . 0 = b2 & b5 . 1 = b3 & b6 . 0 = b3 & b6 . 1 = b4 holds
( b5 + b6 is continuous & (b5 + b6) . 0 = b2 & (b5 + b6) . 1 = b4 )
proof end;

theorem Th28: :: JORDAN20:28
for b1, b2 being non empty Subset of (TOP-REAL 2)
for b3, b4, b5, b6 being Point of (TOP-REAL 2) st b1 is_an_arc_of b3,b4 & b2 is_an_arc_of b5,b6 & LE b5,b6,b1,b3,b4 & b2 c= b1 holds
b2 = Segment b1,b3,b4,b5,b6
proof end;

theorem Th29: :: JORDAN20:29
for b1 being non empty Subset of (TOP-REAL 2)
for b2, b3, b4, b5, b6 being Point of (TOP-REAL 2)
for b7 being Real st b2 `1 < b7 & b3 `1 > b7 & b4 is_Lin b1,b2,b3,b7 & b5 `1 = b7 & LSeg b4,b5 c= b1 & b6 in LSeg b4,b5 holds
b6 is_Lin b1,b2,b3,b7
proof end;

theorem Th30: :: JORDAN20:30
for b1 being non empty Subset of (TOP-REAL 2)
for b2, b3, b4, b5, b6 being Point of (TOP-REAL 2)
for b7 being Real st b2 `1 < b7 & b3 `1 > b7 & b4 is_Rin b1,b2,b3,b7 & b5 `1 = b7 & LSeg b4,b5 c= b1 & b6 in LSeg b4,b5 holds
b6 is_Rin b1,b2,b3,b7
proof end;

theorem Th31: :: JORDAN20:31
for b1 being non empty Subset of (TOP-REAL 2)
for b2, b3, b4, b5, b6 being Point of (TOP-REAL 2)
for b7 being Real st b2 `1 < b7 & b3 `1 > b7 & b4 is_Lout b1,b2,b3,b7 & b5 `1 = b7 & LSeg b4,b5 c= b1 & b6 in LSeg b4,b5 holds
b6 is_Lout b1,b2,b3,b7
proof end;

theorem Th32: :: JORDAN20:32
for b1 being non empty Subset of (TOP-REAL 2)
for b2, b3, b4, b5, b6 being Point of (TOP-REAL 2)
for b7 being Real st b2 `1 < b7 & b3 `1 > b7 & b4 is_Rout b1,b2,b3,b7 & b5 `1 = b7 & LSeg b4,b5 c= b1 & b6 in LSeg b4,b5 holds
b6 is_Rout b1,b2,b3,b7
proof end;

theorem Th33: :: JORDAN20:33
for b1 being non empty Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Real st b1 is_S-P_arc_joining b2,b3 & b2 `1 < b5 & b3 `1 > b5 & b4 in b1 & b4 `1 = b5 & not b4 is_Lin b1,b2,b3,b5 holds
b4 is_Rin b1,b2,b3,b5
proof end;

theorem Th34: :: JORDAN20:34
for b1 being non empty Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Real st b1 is_S-P_arc_joining b2,b3 & b2 `1 < b5 & b3 `1 > b5 & b4 in b1 & b4 `1 = b5 & not b4 is_Lout b1,b2,b3,b5 holds
b4 is_Rout b1,b2,b3,b5
proof end;