:: JORDAN1C semantic presentation

E1: now
let c1 be real number ;
let c2 be Nat;
thus [\(c1 + c2)/] - c2 = ([\c1/] + c2) - c2 by INT_1:51
.= [\c1/] ;
end;

Lemma2: for b1, b2, b3 being real number st b1 <> 0 & b2 <> 0 holds
(b1 / b2) * ((b3 / b1) * b2) = b3
proof end;

Lemma3: for b1 being Point of (TOP-REAL 2) holds b1 is Point of (Euclid 2)
proof end;

Lemma4: for b1 being real number st b1 > 0 holds
2 * (b1 / 4) < b1
proof end;

theorem Th1: :: JORDAN1C:1
canceled;

theorem Th2: :: JORDAN1C:2
for b1 being Simple_closed_curve
for b2, b3, b4 being Nat st [b2,b3] in Indices (Gauge b1,b4) & [(b2 + 1),b3] in Indices (Gauge b1,b4) holds
dist ((Gauge b1,b4) * 1,1),((Gauge b1,b4) * 2,1) = (((Gauge b1,b4) * (b2 + 1),b3) `1 ) - (((Gauge b1,b4) * b2,b3) `1 )
proof end;

theorem Th3: :: JORDAN1C:3
for b1 being Simple_closed_curve
for b2, b3, b4 being Nat st [b2,b3] in Indices (Gauge b1,b4) & [b2,(b3 + 1)] in Indices (Gauge b1,b4) holds
dist ((Gauge b1,b4) * 1,1),((Gauge b1,b4) * 1,2) = (((Gauge b1,b4) * b2,(b3 + 1)) `2 ) - (((Gauge b1,b4) * b2,b3) `2 )
proof end;

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

then Lemma7: TOP-REAL 2 = TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #)
by PCOMPS_1:def 6;

Lemma8: for b1 being Simple_closed_curve
for b2, b3, b4 being Nat
for b5 being Point of (TOP-REAL 2)
for b6 being real number
for b7 being Point of (Euclid 2) st 1 <= b2 & b2 + 1 <= len (Gauge b1,b3) & 1 <= b4 & b4 + 1 <= width (Gauge b1,b3) & b6 > 0 & b5 = b7 & dist ((Gauge b1,b3) * 1,1),((Gauge b1,b3) * 1,2) < b6 / 4 & dist ((Gauge b1,b3) * 1,1),((Gauge b1,b3) * 2,1) < b6 / 4 & b5 in cell (Gauge b1,b3),b2,b4 & (Gauge b1,b3) * b2,b4 in Ball b7,b6 & (Gauge b1,b3) * (b2 + 1),b4 in Ball b7,b6 & (Gauge b1,b3) * b2,(b4 + 1) in Ball b7,b6 & (Gauge b1,b3) * (b2 + 1),(b4 + 1) in Ball b7,b6 holds
cell (Gauge b1,b3),b2,b4 c= Ball b7,b6
proof end;

theorem Th4: :: JORDAN1C:4
for b1 being Subset of (TOP-REAL 2) st b1 is Bounded holds
proj1 .: b1 is bounded
proof end;

theorem Th5: :: JORDAN1C:5
for b1 being non empty compact Subset of (TOP-REAL 2)
for b2, b3 being non empty Subset of (TOP-REAL 2) st b3 = b1 \/ b2 & not proj1 .: b2 is empty & proj1 .: b2 is bounded_below holds
W-bound b3 = min (W-bound b1),(W-bound b2)
proof end;

Lemma10: for b1 being Point of (TOP-REAL 2)
for b2 being Subset of (TOP-REAL 2) st b1 in b2 & b2 is Bounded holds
( inf (proj1 || b2) <= b1 `1 & b1 `1 <= sup (proj1 || b2) )
proof end;

Lemma11: for b1 being Point of (TOP-REAL 2)
for b2 being Subset of (TOP-REAL 2) st b1 in b2 & b2 is Bounded holds
( inf (proj2 || b2) <= b1 `2 & b1 `2 <= sup (proj2 || b2) )
proof end;

theorem Th6: :: JORDAN1C:6
for b1 being Point of (TOP-REAL 2)
for b2 being Subset of (TOP-REAL 2) st b1 in b2 & b2 is Bounded holds
( W-bound b2 <= b1 `1 & b1 `1 <= E-bound b2 & S-bound b2 <= b1 `2 & b1 `2 <= N-bound b2 )
proof end;

theorem Th7: :: JORDAN1C:7
for b1 being Point of (TOP-REAL 2) holds
( b1 in west_halfline b1 & b1 in east_halfline b1 & b1 in north_halfline b1 & b1 in south_halfline b1 )
proof end;

Lemma13: for b1 being Subset of (TOP-REAL 2) st b1 is Bounded holds
for b2 being real number st BDD b1 <> {} & b2 > W-bound (BDD b1) holds
ex b3 being Point of (TOP-REAL 2) st
( b3 in BDD b1 & not b3 `1 >= b2 )
proof end;

Lemma14: for b1 being Subset of (TOP-REAL 2) st b1 is Bounded holds
for b2 being real number st BDD b1 <> {} & b2 < E-bound (BDD b1) holds
ex b3 being Point of (TOP-REAL 2) st
( b3 in BDD b1 & not b3 `1 <= b2 )
proof end;

Lemma15: for b1 being Subset of (TOP-REAL 2) st b1 is Bounded holds
for b2 being real number st BDD b1 <> {} & b2 < N-bound (BDD b1) holds
ex b3 being Point of (TOP-REAL 2) st
( b3 in BDD b1 & not b3 `2 <= b2 )
proof end;

Lemma16: for b1 being Subset of (TOP-REAL 2) st b1 is Bounded holds
for b2 being real number st BDD b1 <> {} & b2 > S-bound (BDD b1) holds
ex b3 being Point of (TOP-REAL 2) st
( b3 in BDD b1 & not b3 `2 >= b2 )
proof end;

theorem Th8: :: JORDAN1C:8
for b1 being Point of (TOP-REAL 2) holds not west_halfline b1 is Bounded
proof end;

theorem Th9: :: JORDAN1C:9
for b1 being Point of (TOP-REAL 2) holds not east_halfline b1 is Bounded
proof end;

theorem Th10: :: JORDAN1C:10
for b1 being Point of (TOP-REAL 2) holds not north_halfline b1 is Bounded
proof end;

theorem Th11: :: JORDAN1C:11
for b1 being Point of (TOP-REAL 2) holds not south_halfline b1 is Bounded
proof end;

E21: now
let c1 be Subset of (TOP-REAL 2);
assume E22: c1 is Bounded ;
then consider c2 being Subset of (TOP-REAL 2) such that
E23: c2 is_outside_component_of c1 and
E24: c2 = UBD c1 by JORDAN2C:76;
E25: UBD c1 is_a_component_of c1 ` by E23, E24, JORDAN2C:def 4;
c1 ` <> {} by E22, JORDAN2C:74;
hence not UBD c1 is empty by E25, SPRECT_1:6;
end;

registration
let c1 be compact Subset of (TOP-REAL 2);
cluster UBD a1 -> non empty ;
coherence
not UBD c1 is empty
proof end;
end;

theorem Th12: :: JORDAN1C:12
for b1 being compact Subset of (TOP-REAL 2) holds UBD b1 is_a_component_of b1 `
proof end;

theorem Th13: :: JORDAN1C:13
for b1 being compact Subset of (TOP-REAL 2)
for b2 being connected Subset of (TOP-REAL 2) st not b2 is Bounded & b2 misses b1 holds
b2 c= UBD b1
proof end;

theorem Th14: :: JORDAN1C:14
for b1 being compact Subset of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st west_halfline b2 misses b1 holds
west_halfline b2 c= UBD b1
proof end;

theorem Th15: :: JORDAN1C:15
for b1 being compact Subset of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st east_halfline b2 misses b1 holds
east_halfline b2 c= UBD b1
proof end;

theorem Th16: :: JORDAN1C:16
for b1 being compact Subset of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st south_halfline b2 misses b1 holds
south_halfline b2 c= UBD b1
proof end;

theorem Th17: :: JORDAN1C:17
for b1 being compact Subset of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st north_halfline b2 misses b1 holds
north_halfline b2 c= UBD b1
proof end;

theorem Th18: :: JORDAN1C:18
for b1 being compact Subset of (TOP-REAL 2) st BDD b1 <> {} holds
W-bound b1 <= W-bound (BDD b1)
proof end;

theorem Th19: :: JORDAN1C:19
for b1 being compact Subset of (TOP-REAL 2) st BDD b1 <> {} holds
E-bound b1 >= E-bound (BDD b1)
proof end;

theorem Th20: :: JORDAN1C:20
for b1 being compact Subset of (TOP-REAL 2) st BDD b1 <> {} holds
S-bound b1 <= S-bound (BDD b1)
proof end;

theorem Th21: :: JORDAN1C:21
for b1 being compact Subset of (TOP-REAL 2) st BDD b1 <> {} holds
N-bound b1 >= N-bound (BDD b1)
proof end;

theorem Th22: :: JORDAN1C:22
for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being compact non vertical Subset of (TOP-REAL 2)
for b4 being Integer st b2 in BDD b3 & b4 = [\(((((b2 `1 ) - (W-bound b3)) / ((E-bound b3) - (W-bound b3))) * (2 |^ b1)) + 2)/] holds
1 < b4
proof end;

theorem Th23: :: JORDAN1C:23
for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being compact non vertical Subset of (TOP-REAL 2)
for b4 being Integer st b2 in BDD b3 & b4 = [\(((((b2 `1 ) - (W-bound b3)) / ((E-bound b3) - (W-bound b3))) * (2 |^ b1)) + 2)/] holds
b4 + 1 <= len (Gauge b3,b1)
proof end;

theorem Th24: :: JORDAN1C:24
for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being compact non horizontal Subset of (TOP-REAL 2)
for b4 being Integer st b2 in BDD b3 & b4 = [\(((((b2 `2 ) - (S-bound b3)) / ((N-bound b3) - (S-bound b3))) * (2 |^ b1)) + 2)/] holds
( 1 < b4 & b4 + 1 <= width (Gauge b3,b1) )
proof end;

theorem Th25: :: JORDAN1C:25
for b1 being Simple_closed_curve
for b2 being Nat
for b3 being Point of (TOP-REAL 2)
for b4 being Integer st b4 = [\(((((b3 `1 ) - (W-bound b1)) / ((E-bound b1) - (W-bound b1))) * (2 |^ b2)) + 2)/] holds
(W-bound b1) + ((((E-bound b1) - (W-bound b1)) / (2 |^ b2)) * (b4 - 2)) <= b3 `1
proof end;

theorem Th26: :: JORDAN1C:26
for b1 being Simple_closed_curve
for b2 being Nat
for b3 being Point of (TOP-REAL 2)
for b4 being Integer st b4 = [\(((((b3 `1 ) - (W-bound b1)) / ((E-bound b1) - (W-bound b1))) * (2 |^ b2)) + 2)/] holds
b3 `1 < (W-bound b1) + ((((E-bound b1) - (W-bound b1)) / (2 |^ b2)) * (b4 - 1))
proof end;

theorem Th27: :: JORDAN1C:27
for b1 being Simple_closed_curve
for b2 being Nat
for b3 being Point of (TOP-REAL 2)
for b4 being Integer st b4 = [\(((((b3 `2 ) - (S-bound b1)) / ((N-bound b1) - (S-bound b1))) * (2 |^ b2)) + 2)/] holds
(S-bound b1) + ((((N-bound b1) - (S-bound b1)) / (2 |^ b2)) * (b4 - 2)) <= b3 `2
proof end;

theorem Th28: :: JORDAN1C:28
for b1 being Simple_closed_curve
for b2 being Nat
for b3 being Point of (TOP-REAL 2)
for b4 being Integer st b4 = [\(((((b3 `2 ) - (S-bound b1)) / ((N-bound b1) - (S-bound b1))) * (2 |^ b2)) + 2)/] holds
b3 `2 < (S-bound b1) + ((((N-bound b1) - (S-bound b1)) / (2 |^ b2)) * (b4 - 1))
proof end;

theorem Th29: :: JORDAN1C:29
for b1 being closed Subset of (TOP-REAL 2)
for b2 being Point of (Euclid 2) st b2 in BDD b1 holds
ex b3 being Real st
( b3 > 0 & Ball b2,b3 c= BDD b1 )
proof end;

theorem Th30: :: JORDAN1C:30
for b1 being Simple_closed_curve
for b2, b3, b4 being Nat
for b5, b6 being Point of (TOP-REAL 2)
for b7 being real number st dist ((Gauge b1,b2) * 1,1),((Gauge b1,b2) * 1,2) < b7 & dist ((Gauge b1,b2) * 1,1),((Gauge b1,b2) * 2,1) < b7 & b5 in cell (Gauge b1,b2),b3,b4 & b6 in cell (Gauge b1,b2),b3,b4 & 1 <= b3 & b3 + 1 <= len (Gauge b1,b2) & 1 <= b4 & b4 + 1 <= width (Gauge b1,b2) holds
dist b5,b6 < 2 * b7
proof end;

theorem Th31: :: JORDAN1C:31
for b1 being Point of (TOP-REAL 2)
for b2 being compact Subset of (TOP-REAL 2) st b1 in BDD b2 holds
b1 `2 <> N-bound (BDD b2)
proof end;

theorem Th32: :: JORDAN1C:32
for b1 being Point of (TOP-REAL 2)
for b2 being compact Subset of (TOP-REAL 2) st b1 in BDD b2 holds
b1 `1 <> E-bound (BDD b2)
proof end;

theorem Th33: :: JORDAN1C:33
for b1 being Point of (TOP-REAL 2)
for b2 being compact Subset of (TOP-REAL 2) st b1 in BDD b2 holds
b1 `2 <> S-bound (BDD b2)
proof end;

theorem Th34: :: JORDAN1C:34
for b1 being Point of (TOP-REAL 2)
for b2 being compact Subset of (TOP-REAL 2) st b1 in BDD b2 holds
b1 `1 <> W-bound (BDD b2)
proof end;

theorem Th35: :: JORDAN1C:35
for b1 being Simple_closed_curve
for b2 being Point of (TOP-REAL 2) st b2 in BDD b1 holds
ex b3, b4, b5 being Nat st
( 1 < b4 & b4 < len (Gauge b1,b3) & 1 < b5 & b5 < width (Gauge b1,b3) & b2 `1 <> ((Gauge b1,b3) * b4,b5) `1 & b2 in cell (Gauge b1,b3),b4,b5 & cell (Gauge b1,b3),b4,b5 c= BDD b1 )
proof end;

theorem Th36: :: JORDAN1C:36
for b1 being Subset of (TOP-REAL 2) st b1 is Bounded holds
not UBD b1 is empty by Lemma21;