begin
Lm2:
for a, b, c being real number st a <> 0 & b <> 0 holds
(a / b) * ((c / a) * b) = c
Lm3:
for p being Point of (TOP-REAL 2) holds p is Point of (Euclid 2)
Lm4:
for r being real number st r > 0 holds
2 * (r / 4) < r
theorem
canceled;
theorem Th2:
for
C being
Simple_closed_curve for
i,
j,
n being
Element of
NAT st
[i,j] in Indices (Gauge C,n) &
[(i + 1),j] in Indices (Gauge C,n) holds
dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 2,1) = (((Gauge C,n) * (i + 1),j) `1 ) - (((Gauge C,n) * i,j) `1 )
theorem Th3:
for
C being
Simple_closed_curve for
i,
j,
n being
Element of
NAT st
[i,j] in Indices (Gauge C,n) &
[i,(j + 1)] in Indices (Gauge C,n) holds
dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 1,2) = (((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 )
TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #)
by EUCLID:def 8;
then Lm5:
TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #)
by PCOMPS_1:def 6;
Lm6:
for C being Simple_closed_curve
for i, n, j being Element of NAT
for p being Point of (TOP-REAL 2)
for r being real number
for q being Point of (Euclid 2) st 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) & r > 0 & p = q & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r / 4 & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r / 4 & p in cell (Gauge C,n),i,j holds
cell (Gauge C,n),i,j c= Ball q,r
theorem Th4:
theorem
Lm7:
for p being Point of (TOP-REAL 2)
for X being Subset of (TOP-REAL 2) st p in X & X is Bounded holds
( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) )
Lm8:
for p being Point of (TOP-REAL 2)
for X being Subset of (TOP-REAL 2) st p in X & X is Bounded holds
( lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )
theorem Th6:
Lm9:
for C being Subset of (TOP-REAL 2) st C is Bounded holds
for h being real number st BDD C <> {} & h > W-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 >= h )
Lm10:
for C being Subset of (TOP-REAL 2) st C is Bounded holds
for h being real number st BDD C <> {} & h < E-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 <= h )
Lm11:
for C being Subset of (TOP-REAL 2) st C is Bounded holds
for h being real number st BDD C <> {} & h < N-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 <= h )
Lm12:
for C being Subset of (TOP-REAL 2) st C is Bounded holds
for h being real number st BDD C <> {} & h > S-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 >= h )
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
for
C being
Simple_closed_curve for
n,
i,
j being
Element of
NAT for
p,
q being
Point of
(TOP-REAL 2) for
r being
real number st
dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 1,2) < r &
dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 2,1) < r &
p in cell (Gauge C,n),
i,
j &
q in cell (Gauge C,n),
i,
j & 1
<= i &
i + 1
<= len (Gauge C,n) & 1
<= j &
j + 1
<= width (Gauge C,n) holds
dist p,
q < 2
* r
theorem
theorem
theorem
theorem Th34:
theorem
for
C being
Simple_closed_curve for
p being
Point of
(TOP-REAL 2) st
p in BDD C holds
ex
n,
i,
j being
Element of
NAT st
( 1
< i &
i < len (Gauge C,n) & 1
< j &
j < width (Gauge C,n) &
p `1 <> ((Gauge C,n) * i,j) `1 &
p in cell (Gauge C,n),
i,
j &
cell (Gauge C,n),
i,
j c= BDD C )
theorem