:: TOPREAL4 semantic presentation

definition
let c1 be Subset of (TOP-REAL 2);
let c2, c3 be Point of (TOP-REAL 2);
pred c1 is_S-P_arc_joining c2,c3 means :Def1: :: TOPREAL4:def 1
ex b1 being FinSequence of (TOP-REAL 2) st
( b1 is_S-Seq & a1 = L~ b1 & a2 = b1 /. 1 & a3 = b1 /. (len b1) );
end;

:: deftheorem Def1 defines is_S-P_arc_joining TOPREAL4:def 1 :
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) holds
( b1 is_S-P_arc_joining b2,b3 iff ex b4 being FinSequence of (TOP-REAL 2) st
( b4 is_S-Seq & b1 = L~ b4 & b2 = b4 /. 1 & b3 = b4 /. (len b4) ) );

definition
let c1 be Subset of (TOP-REAL 2);
attr a1 is being_special_polygon means :: TOPREAL4:def 2
ex b1, b2 being Point of (TOP-REAL 2)ex b3, b4 being Subset of (TOP-REAL 2) st
( b1 <> b2 & b1 in a1 & b2 in a1 & b3 is_S-P_arc_joining b1,b2 & b4 is_S-P_arc_joining b1,b2 & b3 /\ b4 = {b1,b2} & a1 = b3 \/ b4 );
end;

:: deftheorem Def2 defines being_special_polygon TOPREAL4:def 2 :
for b1 being Subset of (TOP-REAL 2) holds
( b1 is being_special_polygon iff ex b2, b3 being Point of (TOP-REAL 2)ex b4, b5 being Subset of (TOP-REAL 2) st
( b2 <> b3 & b2 in b1 & b3 in b1 & b4 is_S-P_arc_joining b2,b3 & b5 is_S-P_arc_joining b2,b3 & b4 /\ b5 = {b2,b3} & b1 = b4 \/ b5 ) );

notation
let c1 be Subset of (TOP-REAL 2);
synonym c1 is_special_polygon for being_special_polygon c1;
end;

definition
let c1 be TopStruct ;
let c2 be Subset of c1;
attr a2 is being_Region means :Def3: :: TOPREAL4:def 3
( a2 is open & a2 is connected );
end;

:: deftheorem Def3 defines being_Region TOPREAL4:def 3 :
for b1 being TopStruct
for b2 being Subset of b1 holds
( b2 is being_Region iff ( b2 is open & b2 is connected ) );

notation
let c1 be TopStruct ;
let c2 be Subset of c1;
synonym c2 is_Region for being_Region c2;
end;

theorem Th1: :: TOPREAL4:1
canceled;

theorem Th2: :: TOPREAL4:2
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_S-P_arc_joining b2,b3 holds
b1 is_S-P_arc
proof end;

theorem Th3: :: TOPREAL4:3
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_S-P_arc_joining b2,b3 holds
b1 is_an_arc_of b2,b3
proof end;

theorem Th4: :: TOPREAL4:4
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_S-P_arc_joining b2,b3 holds
( b2 in b1 & b3 in b1 )
proof end;

theorem Th5: :: TOPREAL4:5
for b1 being Subset of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is_S-P_arc_joining b2,b3 holds
b2 <> b3
proof end;

theorem Th6: :: TOPREAL4:6
for b1 being Subset of (TOP-REAL 2) st b1 is_special_polygon holds
b1 is_simple_closed_curve
proof end;

theorem Th7: :: TOPREAL4:7
for b1, b2 being Point of (TOP-REAL 2)
for b3 being FinSequence of (TOP-REAL 2)
for b4 being Real
for b5 being Point of (Euclid 2) st b1 `1 = b2 `1 & b1 `2 <> b2 `2 & b1 in Ball b5,b4 & b2 in Ball b5,b4 & b3 = <*b1,|[(b1 `1 ),(((b1 `2 ) + (b2 `2 )) / 2)]|,b2*> holds
( b3 is_S-Seq & b3 /. 1 = b1 & b3 /. (len b3) = b2 & L~ b3 is_S-P_arc_joining b1,b2 & L~ b3 c= Ball b5,b4 )
proof end;

theorem Th8: :: TOPREAL4:8
for b1, b2 being Point of (TOP-REAL 2)
for b3 being FinSequence of (TOP-REAL 2)
for b4 being Real
for b5 being Point of (Euclid 2) st b1 `1 <> b2 `1 & b1 `2 = b2 `2 & b1 in Ball b5,b4 & b2 in Ball b5,b4 & b3 = <*b1,|[(((b1 `1 ) + (b2 `1 )) / 2),(b1 `2 )]|,b2*> holds
( b3 is_S-Seq & b3 /. 1 = b1 & b3 /. (len b3) = b2 & L~ b3 is_S-P_arc_joining b1,b2 & L~ b3 c= Ball b5,b4 )
proof end;

theorem Th9: :: TOPREAL4:9
for b1, b2 being Point of (TOP-REAL 2)
for b3 being FinSequence of (TOP-REAL 2)
for b4 being Real
for b5 being Point of (Euclid 2) st b1 `1 <> b2 `1 & b1 `2 <> b2 `2 & b1 in Ball b5,b4 & b2 in Ball b5,b4 & |[(b1 `1 ),(b2 `2 )]| in Ball b5,b4 & b3 = <*b1,|[(b1 `1 ),(b2 `2 )]|,b2*> holds
( b3 is_S-Seq & b3 /. 1 = b1 & b3 /. (len b3) = b2 & L~ b3 is_S-P_arc_joining b1,b2 & L~ b3 c= Ball b5,b4 )
proof end;

theorem Th10: :: TOPREAL4:10
for b1, b2 being Point of (TOP-REAL 2)
for b3 being FinSequence of (TOP-REAL 2)
for b4 being Real
for b5 being Point of (Euclid 2) st b1 `1 <> b2 `1 & b1 `2 <> b2 `2 & b1 in Ball b5,b4 & b2 in Ball b5,b4 & |[(b2 `1 ),(b1 `2 )]| in Ball b5,b4 & b3 = <*b1,|[(b2 `1 ),(b1 `2 )]|,b2*> holds
( b3 is_S-Seq & b3 /. 1 = b1 & b3 /. (len b3) = b2 & L~ b3 is_S-P_arc_joining b1,b2 & L~ b3 c= Ball b5,b4 )
proof end;

theorem Th11: :: TOPREAL4:11
for b1, b2 being Point of (TOP-REAL 2)
for b3 being Real
for b4 being Point of (Euclid 2) st b1 <> b2 & b1 in Ball b4,b3 & b2 in Ball b4,b3 holds
ex b5 being Subset of (TOP-REAL 2) st
( b5 is_S-P_arc_joining b1,b2 & b5 c= Ball b4,b3 )
proof end;

theorem Th12: :: TOPREAL4:12
for b1 being Point of (TOP-REAL 2)
for b2, b3 being FinSequence of (TOP-REAL 2) st b1 <> b2 /. 1 & (b2 /. 1) `2 = b1 `2 & b2 is_S-Seq & b1 in LSeg b2,1 & b3 = <*(b2 /. 1),|[((((b2 /. 1) `1 ) + (b1 `1 )) / 2),((b2 /. 1) `2 )]|,b1*> holds
( b3 is_S-Seq & b3 /. 1 = b2 /. 1 & b3 /. (len b3) = b1 & L~ b3 is_S-P_arc_joining b2 /. 1,b1 & L~ b3 c= L~ b2 & L~ b3 = (L~ (b2 | 1)) \/ (LSeg (b2 /. 1),b1) )
proof end;

theorem Th13: :: TOPREAL4:13
for b1 being Point of (TOP-REAL 2)
for b2, b3 being FinSequence of (TOP-REAL 2) st b1 <> b2 /. 1 & (b2 /. 1) `1 = b1 `1 & b2 is_S-Seq & b1 in LSeg b2,1 & b3 = <*(b2 /. 1),|[((b2 /. 1) `1 ),((((b2 /. 1) `2 ) + (b1 `2 )) / 2)]|,b1*> holds
( b3 is_S-Seq & b3 /. 1 = b2 /. 1 & b3 /. (len b3) = b1 & L~ b3 is_S-P_arc_joining b2 /. 1,b1 & L~ b3 c= L~ b2 & L~ b3 = (L~ (b2 | 1)) \/ (LSeg (b2 /. 1),b1) )
proof end;

theorem Th14: :: TOPREAL4:14
for b1 being Point of (TOP-REAL 2)
for b2, b3 being FinSequence of (TOP-REAL 2)
for b4 being Nat st b1 <> b2 /. 1 & b2 is_S-Seq & b4 in dom b2 & b4 + 1 in dom b2 & b4 > 1 & b1 in LSeg b2,b4 & b1 <> b2 /. b4 & b1 <> b2 /. (b4 + 1) & b3 = (b2 | b4) ^ <*b1*> holds
( b3 is_S-Seq & b3 /. 1 = b2 /. 1 & b3 /. (len b3) = b1 & L~ b3 is_S-P_arc_joining b2 /. 1,b1 & L~ b3 c= L~ b2 & L~ b3 = (L~ (b2 | b4)) \/ (LSeg (b2 /. b4),b1) )
proof end;

theorem Th15: :: TOPREAL4:15
for b1, b2 being FinSequence of (TOP-REAL 2) st b1 /. 2 <> b1 /. 1 & b1 is_S-Seq & (b1 /. 2) `2 = (b1 /. 1) `2 & b2 = <*(b1 /. 1),|[((((b1 /. 1) `1 ) + ((b1 /. 2) `1 )) / 2),((b1 /. 1) `2 )]|,(b1 /. 2)*> holds
( b2 is_S-Seq & b2 /. 1 = b1 /. 1 & b2 /. (len b2) = b1 /. 2 & L~ b2 is_S-P_arc_joining b1 /. 1,b1 /. 2 & L~ b2 c= L~ b1 & L~ b2 = (L~ (b1 | 1)) \/ (LSeg (b1 /. 1),(b1 /. 2)) & L~ b2 = (L~ (b1 | 2)) \/ (LSeg (b1 /. 2),(b1 /. 2)) )
proof end;

theorem Th16: :: TOPREAL4:16
for b1, b2 being FinSequence of (TOP-REAL 2) st b1 /. 2 <> b1 /. 1 & b1 is_S-Seq & (b1 /. 2) `1 = (b1 /. 1) `1 & b2 = <*(b1 /. 1),|[((b1 /. 1) `1 ),((((b1 /. 1) `2 ) + ((b1 /. 2) `2 )) / 2)]|,(b1 /. 2)*> holds
( b2 is_S-Seq & b2 /. 1 = b1 /. 1 & b2 /. (len b2) = b1 /. 2 & L~ b2 is_S-P_arc_joining b1 /. 1,b1 /. 2 & L~ b2 c= L~ b1 & L~ b2 = (L~ (b1 | 1)) \/ (LSeg (b1 /. 1),(b1 /. 2)) & L~ b2 = (L~ (b1 | 2)) \/ (LSeg (b1 /. 2),(b1 /. 2)) )
proof end;

theorem Th17: :: TOPREAL4:17
for b1, b2 being FinSequence of (TOP-REAL 2)
for b3 being Nat st b1 /. b3 <> b1 /. 1 & b1 is_S-Seq & b3 > 2 & b3 in dom b1 & b2 = b1 | b3 holds
( b2 is_S-Seq & b2 /. 1 = b1 /. 1 & b2 /. (len b2) = b1 /. b3 & L~ b2 is_S-P_arc_joining b1 /. 1,b1 /. b3 & L~ b2 c= L~ b1 & L~ b2 = (L~ (b1 | b3)) \/ (LSeg (b1 /. b3),(b1 /. b3)) )
proof end;

theorem Th18: :: TOPREAL4:18
for b1 being Point of (TOP-REAL 2)
for b2 being FinSequence of (TOP-REAL 2)
for b3 being Nat st b1 <> b2 /. 1 & b2 is_S-Seq & b1 in LSeg b2,b3 holds
ex b4 being FinSequence of (TOP-REAL 2) st
( b4 is_S-Seq & b4 /. 1 = b2 /. 1 & b4 /. (len b4) = b1 & L~ b4 is_S-P_arc_joining b2 /. 1,b1 & L~ b4 c= L~ b2 & L~ b4 = (L~ (b2 | b3)) \/ (LSeg (b2 /. b3),b1) )
proof end;

theorem Th19: :: TOPREAL4:19
for b1 being Point of (TOP-REAL 2)
for b2 being FinSequence of (TOP-REAL 2) st b1 <> b2 /. 1 & b2 is_S-Seq & b1 in L~ b2 holds
ex b3 being FinSequence of (TOP-REAL 2) st
( b3 is_S-Seq & b3 /. 1 = b2 /. 1 & b3 /. (len b3) = b1 & L~ b3 is_S-P_arc_joining b2 /. 1,b1 & L~ b3 c= L~ b2 )
proof end;

theorem Th20: :: TOPREAL4:20
for b1 being Point of (TOP-REAL 2)
for b2, b3 being FinSequence of (TOP-REAL 2)
for b4 being Real
for b5 being Point of (Euclid 2) st ( ( b1 `1 = (b2 /. (len b2)) `1 & b1 `2 <> (b2 /. (len b2)) `2 ) or ( b1 `1 <> (b2 /. (len b2)) `1 & b1 `2 = (b2 /. (len b2)) `2 ) ) & not b2 /. 1 in Ball b5,b4 & b2 /. (len b2) in Ball b5,b4 & b1 in Ball b5,b4 & b2 is_S-Seq & (LSeg (b2 /. (len b2)),b1) /\ (L~ b2) = {(b2 /. (len b2))} & b3 = b2 ^ <*b1*> holds
( b3 is_S-Seq & L~ b3 is_S-P_arc_joining b2 /. 1,b1 & L~ b3 c= (L~ b2) \/ (Ball b5,b4) )
proof end;

theorem Th21: :: TOPREAL4:21
for b1 being Point of (TOP-REAL 2)
for b2, b3 being FinSequence of (TOP-REAL 2)
for b4 being Real
for b5 being Point of (Euclid 2) st not b2 /. 1 in Ball b5,b4 & b2 /. (len b2) in Ball b5,b4 & b1 in Ball b5,b4 & |[(b1 `1 ),((b2 /. (len b2)) `2 )]| in Ball b5,b4 & b2 is_S-Seq & b1 `1 <> (b2 /. (len b2)) `1 & b1 `2 <> (b2 /. (len b2)) `2 & b3 = b2 ^ <*|[(b1 `1 ),((b2 /. (len b2)) `2 )]|,b1*> & ((LSeg (b2 /. (len b2)),|[(b1 `1 ),((b2 /. (len b2)) `2 )]|) \/ (LSeg |[(b1 `1 ),((b2 /. (len b2)) `2 )]|,b1)) /\ (L~ b2) = {(b2 /. (len b2))} holds
( L~ b3 is_S-P_arc_joining b2 /. 1,b1 & L~ b3 c= (L~ b2) \/ (Ball b5,b4) )
proof end;

theorem Th22: :: TOPREAL4:22
for b1 being Point of (TOP-REAL 2)
for b2, b3 being FinSequence of (TOP-REAL 2)
for b4 being Real
for b5 being Point of (Euclid 2) st not b2 /. 1 in Ball b5,b4 & b2 /. (len b2) in Ball b5,b4 & b1 in Ball b5,b4 & |[((b2 /. (len b2)) `1 ),(b1 `2 )]| in Ball b5,b4 & b2 is_S-Seq & b1 `1 <> (b2 /. (len b2)) `1 & b1 `2 <> (b2 /. (len b2)) `2 & b3 = b2 ^ <*|[((b2 /. (len b2)) `1 ),(b1 `2 )]|,b1*> & ((LSeg (b2 /. (len b2)),|[((b2 /. (len b2)) `1 ),(b1 `2 )]|) \/ (LSeg |[((b2 /. (len b2)) `1 ),(b1 `2 )]|,b1)) /\ (L~ b2) = {(b2 /. (len b2))} holds
( L~ b3 is_S-P_arc_joining b2 /. 1,b1 & L~ b3 c= (L~ b2) \/ (Ball b5,b4) )
proof end;

theorem Th23: :: TOPREAL4:23
for b1 being Point of (TOP-REAL 2)
for b2 being FinSequence of (TOP-REAL 2)
for b3 being Real
for b4 being Point of (Euclid 2) st not b2 /. 1 in Ball b4,b3 & b2 /. (len b2) in Ball b4,b3 & b1 in Ball b4,b3 & b2 is_S-Seq & not b1 in L~ b2 holds
ex b5 being FinSequence of (TOP-REAL 2) st
( L~ b5 is_S-P_arc_joining b2 /. 1,b1 & L~ b5 c= (L~ b2) \/ (Ball b4,b3) )
proof end;

theorem Th24: :: TOPREAL4:24
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4 being Point of (TOP-REAL 2)
for b5 being Subset of (TOP-REAL 2)
for b6 being Real
for b7 being Point of (Euclid 2) st b2 <> b3 & b5 is_S-P_arc_joining b3,b4 & b5 c= b1 & b2 in Ball b7,b6 & b4 in Ball b7,b6 & Ball b7,b6 c= b1 holds
ex b8 being Subset of (TOP-REAL 2) st
( b8 is_S-P_arc_joining b3,b2 & b8 c= b1 )
proof end;

Lemma24: TopSpaceMetr (Euclid 2) = TOP-REAL 2
by EUCLID:def 8;

theorem Th25: :: TOPREAL4:25
for b1, b2 being Subset of (TOP-REAL 2)
for b3 being Point of (TOP-REAL 2) st b1 is_Region & b2 = { b4 where B is Point of (TOP-REAL 2) : ( b4 <> b3 & b4 in b1 & ( for b1 being Subset of (TOP-REAL 2) holds
( not b5 is_S-P_arc_joining b3,b4 or not b5 c= b1 ) ) ) } holds
b2 is open
proof end;

theorem Th26: :: TOPREAL4:26
for b1 being Point of (TOP-REAL 2)
for b2, b3 being Subset of (TOP-REAL 2) st b2 is_Region & b1 in b2 & b3 = { b4 where B is Point of (TOP-REAL 2) : ( b4 = b1 or ex b1 being Subset of (TOP-REAL 2) st
( b5 is_S-P_arc_joining b1,b4 & b5 c= b2 ) ) } holds
b3 is open
proof end;

theorem Th27: :: TOPREAL4:27
for b1 being Point of (TOP-REAL 2)
for b2, b3 being Subset of (TOP-REAL 2) st b1 in b2 & b3 = { b4 where B is Point of (TOP-REAL 2) : ( b4 = b1 or ex b1 being Subset of (TOP-REAL 2) st
( b5 is_S-P_arc_joining b1,b4 & b5 c= b2 ) ) } holds
b3 c= b2
proof end;

theorem Th28: :: TOPREAL4:28
for b1 being Point of (TOP-REAL 2)
for b2, b3 being Subset of (TOP-REAL 2) st b2 is_Region & b1 in b2 & b3 = { b4 where B is Point of (TOP-REAL 2) : ( b4 = b1 or ex b1 being Subset of (TOP-REAL 2) st
( b5 is_S-P_arc_joining b1,b4 & b5 c= b2 ) ) } holds
b2 c= b3
proof end;

theorem Th29: :: TOPREAL4:29
for b1 being Point of (TOP-REAL 2)
for b2, b3 being Subset of (TOP-REAL 2) st b2 is_Region & b1 in b2 & b3 = { b4 where B is Point of (TOP-REAL 2) : ( b4 = b1 or ex b1 being Subset of (TOP-REAL 2) st
( b5 is_S-P_arc_joining b1,b4 & b5 c= b2 ) ) } holds
b2 = b3
proof end;

theorem Th30: :: TOPREAL4:30
for b1, b2 being Point of (TOP-REAL 2)
for b3 being Subset of (TOP-REAL 2) st b3 is_Region & b1 in b3 & b2 in b3 & b1 <> b2 holds
ex b4 being Subset of (TOP-REAL 2) st
( b4 is_S-P_arc_joining b1,b2 & b4 c= b3 )
proof end;