:: JORDAN21 semantic presentation

Lemma1: dom proj2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;

Lemma2: for b1 being real number
for b2 being Subset of (TOP-REAL 2) st b1 in proj2 .: b2 holds
ex b3 being Point of (TOP-REAL 2) st
( b3 in b2 & proj2 . b3 = b1 )
proof end;

E3: now
let c1, c2, c3, c4 be set ;
assume c1 in (c2 \/ c3) \/ c4 ;
then ( c1 in c2 \/ c3 or c1 in c4 ) by XBOOLE_0:def 2;
hence ( c1 in c2 or c1 in c3 or c1 in c4 ) by XBOOLE_0:def 2;
end;

Lemma4: for b1, b2, b3, b4 being set st b1 misses b4 & b2 misses b4 & b3 misses b4 holds
(b1 \/ b2) \/ b3 misses b4
proof end;

theorem Th1: :: JORDAN21:1
for b1 being Nat
for b2 being Point of (TOP-REAL b1) holds {b2} is Bounded
proof end;

theorem Th2: :: JORDAN21:2
for b1, b2 being real number
for b3 being Subset of (TOP-REAL 2) st b3 = { |[b4,b2]| where B is Real : b1 < b4 } holds
b3 is convex
proof end;

theorem Th3: :: JORDAN21:3
for b1, b2 being real number
for b3 being Subset of (TOP-REAL 2) st b3 = { |[b4,b2]| where B is Real : b4 < b1 } holds
b3 is convex
proof end;

theorem Th4: :: JORDAN21:4
for b1, b2 being real number
for b3 being Subset of (TOP-REAL 2) st b3 = { |[b1,b4]| where B is Real : b2 < b4 } holds
b3 is convex
proof end;

theorem Th5: :: JORDAN21:5
for b1, b2 being real number
for b3 being Subset of (TOP-REAL 2) st b3 = { |[b1,b4]| where B is Real : b4 < b2 } holds
b3 is convex
proof end;

theorem Th6: :: JORDAN21:6
for b1 being Point of (TOP-REAL 2) holds (north_halfline b1) \ {b1} is convex
proof end;

theorem Th7: :: JORDAN21:7
for b1 being Point of (TOP-REAL 2) holds (south_halfline b1) \ {b1} is convex
proof end;

theorem Th8: :: JORDAN21:8
for b1 being Point of (TOP-REAL 2) holds (west_halfline b1) \ {b1} is convex
proof end;

theorem Th9: :: JORDAN21:9
for b1 being Point of (TOP-REAL 2) holds (east_halfline b1) \ {b1} is convex
proof end;

theorem Th10: :: JORDAN21:10
for b1 being Subset of the carrier of (TOP-REAL 2) holds UBD b1 misses b1
proof end;

theorem Th11: :: JORDAN21:11
for b1 being Subset of the carrier of (TOP-REAL 2)
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 & b2 <> b4 & b3 <> b5 holds
( not b2 in Segment b1,b2,b3,b4,b5 & not b3 in Segment b1,b2,b3,b4,b5 )
proof end;

definition
let c1 be Subset of (TOP-REAL 2);
attr a1 is with_the_max_arc means :Def1: :: JORDAN21:def 1
a1 meets Vertical_Line (((W-bound a1) + (E-bound a1)) / 2);
end;

:: deftheorem Def1 defines with_the_max_arc JORDAN21:def 1 :
for b1 being Subset of (TOP-REAL 2) holds
( b1 is with_the_max_arc iff b1 meets Vertical_Line (((W-bound b1) + (E-bound b1)) / 2) );

registration
cluster with_the_max_arc -> non empty Element of K40(the carrier of (TOP-REAL 2));
coherence
for b1 being Subset of (TOP-REAL 2) st b1 is with_the_max_arc holds
not b1 is empty
proof end;
end;

Lemma15: for b1 being Simple_closed_curve holds Upper_Middle_Point b1 in b1
proof end;

registration
cluster -> non empty with_the_max_arc Element of K40(the carrier of (TOP-REAL 2));
coherence
for b1 being Simple_closed_curve holds b1 is with_the_max_arc
proof end;
end;

registration
cluster non empty with_the_max_arc Element of K40(the carrier of (TOP-REAL 2));
existence
not for b1 being Simple_closed_curve holds b1 is empty
proof end;
end;

theorem Th12: :: JORDAN21:12
for b1 being with_the_max_arc Subset of (TOP-REAL 2) holds not proj2 .: (b1 /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) is empty
proof end;

theorem Th13: :: JORDAN21:13
for b1 being compact Subset of (TOP-REAL 2) holds
( proj2 .: (b1 /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) is closed & proj2 .: (b1 /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) is bounded_below & proj2 .: (b1 /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) is bounded_above )
proof end;

Lemma18: for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Nat holds 1 <= len (Gauge b1,b2)
proof end;

theorem Th14: :: JORDAN21:14
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Nat holds [1,1] in Indices (Gauge b1,b2)
proof end;

theorem Th15: :: JORDAN21:15
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Nat holds [1,2] in Indices (Gauge b1,b2)
proof end;

theorem Th16: :: JORDAN21:16
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Nat holds [2,1] in Indices (Gauge b1,b2)
proof end;

theorem Th17: :: JORDAN21:17
for b1, b2, b3, b4 being Nat
for b5 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 > b2 & [b3,b4] in Indices (Gauge b5,b2) & [b3,(b4 + 1)] in Indices (Gauge b5,b2) holds
dist ((Gauge b5,b1) * b3,b4),((Gauge b5,b1) * b3,(b4 + 1)) < dist ((Gauge b5,b2) * b3,b4),((Gauge b5,b2) * b3,(b4 + 1))
proof end;

theorem Th18: :: JORDAN21:18
for b1, b2 being Nat
for b3 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 > b2 holds
dist ((Gauge b3,b1) * 1,1),((Gauge b3,b1) * 1,2) < dist ((Gauge b3,b2) * 1,1),((Gauge b3,b2) * 1,2)
proof end;

theorem Th19: :: JORDAN21:19
for b1, b2, b3, b4 being Nat
for b5 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 > b2 & [b3,b4] in Indices (Gauge b5,b2) & [(b3 + 1),b4] in Indices (Gauge b5,b2) holds
dist ((Gauge b5,b1) * b3,b4),((Gauge b5,b1) * (b3 + 1),b4) < dist ((Gauge b5,b2) * b3,b4),((Gauge b5,b2) * (b3 + 1),b4)
proof end;

theorem Th20: :: JORDAN21:20
for b1, b2 being Nat
for b3 being compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 > b2 holds
dist ((Gauge b3,b1) * 1,1),((Gauge b3,b1) * 2,1) < dist ((Gauge b3,b2) * 1,1),((Gauge b3,b2) * 2,1)
proof end;

theorem Th21: :: JORDAN21:21
for b1 being Simple_closed_curve
for b2 being Nat
for b3, b4 being real number st b3 > 0 & b4 > 0 holds
ex b5 being Nat st
( b2 < b5 & dist ((Gauge b1,b5) * 1,1),((Gauge b1,b5) * 1,2) < b3 & dist ((Gauge b1,b5) * 1,1),((Gauge b1,b5) * 2,1) < b4 )
proof end;

theorem Th22: :: JORDAN21:22
for b1 being Simple_closed_curve holds Upper_Middle_Point b1 in b1 by Lemma15;

theorem Th23: :: JORDAN21:23
for b1 being Simple_closed_curve holds Lower_Middle_Point b1 in b1
proof end;

theorem Th24: :: JORDAN21:24
for b1 being Simple_closed_curve holds (Lower_Middle_Point b1) `2 <> (Upper_Middle_Point b1) `2
proof end;

theorem Th25: :: JORDAN21:25
for b1 being Simple_closed_curve holds Lower_Middle_Point b1 <> Upper_Middle_Point b1
proof end;

theorem Th26: :: JORDAN21:26
for b1 being Simple_closed_curve holds W-bound b1 = W-bound (Upper_Arc b1)
proof end;

theorem Th27: :: JORDAN21:27
for b1 being Simple_closed_curve holds E-bound b1 = E-bound (Upper_Arc b1)
proof end;

theorem Th28: :: JORDAN21:28
for b1 being Simple_closed_curve holds W-bound b1 = W-bound (Lower_Arc b1)
proof end;

theorem Th29: :: JORDAN21:29
for b1 being Simple_closed_curve holds E-bound b1 = E-bound (Lower_Arc b1)
proof end;

theorem Th30: :: JORDAN21:30
for b1 being Simple_closed_curve holds
( not (Upper_Arc b1) /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2)) is empty & not proj2 .: ((Upper_Arc b1) /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) is empty )
proof end;

theorem Th31: :: JORDAN21:31
for b1 being Simple_closed_curve holds
( not (Lower_Arc b1) /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2)) is empty & not proj2 .: ((Lower_Arc b1) /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) is empty )
proof end;

theorem Th32: :: JORDAN21:32
for b1 being Simple_closed_curve
for b2 being connected compact Subset of (TOP-REAL 2) st b2 c= b1 & W-min b1 in b2 & E-max b1 in b2 & not Upper_Arc b1 c= b2 holds
Lower_Arc b1 c= b2
proof end;

definition
let c1 be Subset of the carrier of (TOP-REAL 2);
func UMP c1 -> Point of (TOP-REAL 2) equals :: JORDAN21:def 2
|[(((E-bound a1) + (W-bound a1)) / 2),(sup (proj2 .: (a1 /\ (Vertical_Line (((E-bound a1) + (W-bound a1)) / 2)))))]|;
correctness
coherence
|[(((E-bound c1) + (W-bound c1)) / 2),(sup (proj2 .: (c1 /\ (Vertical_Line (((E-bound c1) + (W-bound c1)) / 2)))))]| is Point of (TOP-REAL 2);
;
func LMP c1 -> Point of (TOP-REAL 2) equals :: JORDAN21:def 3
|[(((E-bound a1) + (W-bound a1)) / 2),(inf (proj2 .: (a1 /\ (Vertical_Line (((E-bound a1) + (W-bound a1)) / 2)))))]|;
correctness
coherence
|[(((E-bound c1) + (W-bound c1)) / 2),(inf (proj2 .: (c1 /\ (Vertical_Line (((E-bound c1) + (W-bound c1)) / 2)))))]| is Point of (TOP-REAL 2);
;
end;

:: deftheorem Def2 defines UMP JORDAN21:def 2 :
for b1 being Subset of the carrier of (TOP-REAL 2) holds UMP b1 = |[(((E-bound b1) + (W-bound b1)) / 2),(sup (proj2 .: (b1 /\ (Vertical_Line (((E-bound b1) + (W-bound b1)) / 2)))))]|;

:: deftheorem Def3 defines LMP JORDAN21:def 3 :
for b1 being Subset of the carrier of (TOP-REAL 2) holds LMP b1 = |[(((E-bound b1) + (W-bound b1)) / 2),(inf (proj2 .: (b1 /\ (Vertical_Line (((E-bound b1) + (W-bound b1)) / 2)))))]|;

theorem Th33: :: JORDAN21:33
for b1 being Subset of (TOP-REAL 2) holds (UMP b1) `1 = ((W-bound b1) + (E-bound b1)) / 2 by EUCLID:56;

theorem Th34: :: JORDAN21:34
for b1 being Subset of (TOP-REAL 2) holds (UMP b1) `2 = sup (proj2 .: (b1 /\ (Vertical_Line (((E-bound b1) + (W-bound b1)) / 2)))) by EUCLID:56;

theorem Th35: :: JORDAN21:35
for b1 being Subset of (TOP-REAL 2) holds (LMP b1) `1 = ((W-bound b1) + (E-bound b1)) / 2 by EUCLID:56;

theorem Th36: :: JORDAN21:36
for b1 being Subset of (TOP-REAL 2) holds (LMP b1) `2 = inf (proj2 .: (b1 /\ (Vertical_Line (((E-bound b1) + (W-bound b1)) / 2)))) by EUCLID:56;

theorem Th37: :: JORDAN21:37
for b1 being compact non vertical Subset of (TOP-REAL 2) holds UMP b1 <> W-min b1
proof end;

theorem Th38: :: JORDAN21:38
for b1 being compact non vertical Subset of (TOP-REAL 2) holds UMP b1 <> E-max b1
proof end;

theorem Th39: :: JORDAN21:39
for b1 being compact non vertical Subset of (TOP-REAL 2) holds LMP b1 <> W-min b1
proof end;

theorem Th40: :: JORDAN21:40
for b1 being compact non vertical Subset of (TOP-REAL 2) holds LMP b1 <> E-max b1
proof end;

theorem Th41: :: JORDAN21:41
for b1 being Point of (TOP-REAL 2)
for b2 being compact Subset of (TOP-REAL 2) st b1 in b2 /\ (Vertical_Line (((W-bound b2) + (E-bound b2)) / 2)) holds
b1 `2 <= (UMP b2) `2
proof end;

theorem Th42: :: JORDAN21:42
for b1 being Point of (TOP-REAL 2)
for b2 being compact Subset of (TOP-REAL 2) st b1 in b2 /\ (Vertical_Line (((W-bound b2) + (E-bound b2)) / 2)) holds
(LMP b2) `2 <= b1 `2
proof end;

theorem Th43: :: JORDAN21:43
for b1 being compact with_the_max_arc Subset of (TOP-REAL 2) holds UMP b1 in b1
proof end;

theorem Th44: :: JORDAN21:44
for b1 being compact with_the_max_arc Subset of (TOP-REAL 2) holds LMP b1 in b1
proof end;

theorem Th45: :: JORDAN21:45
for b1 being Subset of (TOP-REAL 2) holds LSeg (UMP b1),|[(((W-bound b1) + (E-bound b1)) / 2),(N-bound b1)]| is vertical
proof end;

theorem Th46: :: JORDAN21:46
for b1 being Subset of (TOP-REAL 2) holds LSeg (LMP b1),|[(((W-bound b1) + (E-bound b1)) / 2),(S-bound b1)]| is vertical
proof end;

theorem Th47: :: JORDAN21:47
for b1 being compact with_the_max_arc Subset of (TOP-REAL 2) holds (LSeg (UMP b1),|[(((W-bound b1) + (E-bound b1)) / 2),(N-bound b1)]|) /\ b1 = {(UMP b1)}
proof end;

theorem Th48: :: JORDAN21:48
for b1 being compact with_the_max_arc Subset of (TOP-REAL 2) holds (LSeg (LMP b1),|[(((W-bound b1) + (E-bound b1)) / 2),(S-bound b1)]|) /\ b1 = {(LMP b1)}
proof end;

theorem Th49: :: JORDAN21:49
for b1 being Simple_closed_curve holds (LMP b1) `2 < (UMP b1) `2
proof end;

theorem Th50: :: JORDAN21:50
for b1 being Simple_closed_curve holds UMP b1 <> LMP b1
proof end;

theorem Th51: :: JORDAN21:51
for b1 being Simple_closed_curve holds S-bound b1 < (UMP b1) `2
proof end;

theorem Th52: :: JORDAN21:52
for b1 being Simple_closed_curve holds (UMP b1) `2 <= N-bound b1
proof end;

theorem Th53: :: JORDAN21:53
for b1 being Simple_closed_curve holds S-bound b1 <= (LMP b1) `2
proof end;

theorem Th54: :: JORDAN21:54
for b1 being Simple_closed_curve holds (LMP b1) `2 < N-bound b1
proof end;

theorem Th55: :: JORDAN21:55
for b1 being Simple_closed_curve holds LSeg (UMP b1),|[(((W-bound b1) + (E-bound b1)) / 2),(N-bound b1)]| misses LSeg (LMP b1),|[(((W-bound b1) + (E-bound b1)) / 2),(S-bound b1)]|
proof end;

theorem Th56: :: JORDAN21:56
for b1, b2 being Subset of (TOP-REAL 2) st b1 c= b2 & (W-bound b1) + (E-bound b1) = (W-bound b2) + (E-bound b2) & not b1 /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2)) is empty & proj2 .: (b2 /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) is bounded_above holds
(UMP b1) `2 <= (UMP b2) `2
proof end;

theorem Th57: :: JORDAN21:57
for b1, b2 being Subset of (TOP-REAL 2) st b1 c= b2 & (W-bound b1) + (E-bound b1) = (W-bound b2) + (E-bound b2) & not b1 /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2)) is empty & proj2 .: (b2 /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2))) is bounded_below holds
(LMP b2) `2 <= (LMP b1) `2
proof end;

theorem Th58: :: JORDAN21:58
for b1, b2 being Subset of (TOP-REAL 2) st b1 c= b2 & UMP b2 in b1 & not b1 /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2)) is empty & proj2 .: (b2 /\ (Vertical_Line (((W-bound b2) + (E-bound b2)) / 2))) is bounded_above & (W-bound b1) + (E-bound b1) = (W-bound b2) + (E-bound b2) holds
UMP b1 = UMP b2
proof end;

theorem Th59: :: JORDAN21:59
for b1, b2 being Subset of (TOP-REAL 2) st b1 c= b2 & LMP b2 in b1 & not b1 /\ (Vertical_Line (((W-bound b1) + (E-bound b1)) / 2)) is empty & proj2 .: (b2 /\ (Vertical_Line (((W-bound b2) + (E-bound b2)) / 2))) is bounded_below & (W-bound b1) + (E-bound b1) = (W-bound b2) + (E-bound b2) holds
LMP b1 = LMP b2
proof end;

theorem Th60: :: JORDAN21:60
for b1 being Simple_closed_curve holds (UMP (Upper_Arc b1)) `2 <= N-bound b1
proof end;

theorem Th61: :: JORDAN21:61
for b1 being Simple_closed_curve holds S-bound b1 <= (LMP (Lower_Arc b1)) `2
proof end;

theorem Th62: :: JORDAN21:62
for b1 being Simple_closed_curve holds
( not LMP b1 in Lower_Arc b1 or not UMP b1 in Lower_Arc b1 )
proof end;

theorem Th63: :: JORDAN21:63
for b1 being Simple_closed_curve holds
( not LMP b1 in Upper_Arc b1 or not UMP b1 in Upper_Arc b1 )
proof end;

theorem Th64: :: JORDAN21:64
for b1 being Simple_closed_curve
for b2 being Nat st 0 < b2 holds
sup (proj2 .: ((L~ (Cage b1,b2)) /\ (LSeg ((Gauge b1,b2) * (Center (Gauge b1,b2)),1),((Gauge b1,b2) * (Center (Gauge b1,b2)),(len (Gauge b1,b2)))))) = sup (proj2 .: ((L~ (Cage b1,b2)) /\ (Vertical_Line (((E-bound (L~ (Cage b1,b2))) + (W-bound (L~ (Cage b1,b2)))) / 2))))
proof end;

theorem Th65: :: JORDAN21:65
for b1 being Simple_closed_curve
for b2 being Nat st 0 < b2 holds
inf (proj2 .: ((L~ (Cage b1,b2)) /\ (LSeg ((Gauge b1,b2) * (Center (Gauge b1,b2)),1),((Gauge b1,b2) * (Center (Gauge b1,b2)),(len (Gauge b1,b2)))))) = inf (proj2 .: ((L~ (Cage b1,b2)) /\ (Vertical_Line (((E-bound (L~ (Cage b1,b2))) + (W-bound (L~ (Cage b1,b2)))) / 2))))
proof end;

theorem Th66: :: JORDAN21:66
for b1 being Simple_closed_curve
for b2 being Nat st 0 < b2 holds
UMP (L~ (Cage b1,b2)) = |[(((E-bound (L~ (Cage b1,b2))) + (W-bound (L~ (Cage b1,b2)))) / 2),(sup (proj2 .: ((L~ (Cage b1,b2)) /\ (LSeg ((Gauge b1,b2) * (Center (Gauge b1,b2)),1),((Gauge b1,b2) * (Center (Gauge b1,b2)),(len (Gauge b1,b2)))))))]| by Th64;

theorem Th67: :: JORDAN21:67
for b1 being Simple_closed_curve
for b2 being Nat st 0 < b2 holds
LMP (L~ (Cage b1,b2)) = |[(((E-bound (L~ (Cage b1,b2))) + (W-bound (L~ (Cage b1,b2)))) / 2),(inf (proj2 .: ((L~ (Cage b1,b2)) /\ (LSeg ((Gauge b1,b2) * (Center (Gauge b1,b2)),1),((Gauge b1,b2) * (Center (Gauge b1,b2)),(len (Gauge b1,b2)))))))]| by Th65;

theorem Th68: :: JORDAN21:68
for b1 being Simple_closed_curve
for b2 being Nat holds (UMP b1) `2 < (UMP (L~ (Cage b1,b2))) `2
proof end;

theorem Th69: :: JORDAN21:69
for b1 being Simple_closed_curve
for b2 being Nat holds (LMP b1) `2 > (LMP (L~ (Cage b1,b2))) `2
proof end;

registration
let c1 be Simple_closed_curve;
cluster Lower_Arc a1 -> with_the_max_arc ;
coherence
Lower_Arc c1 is with_the_max_arc
proof end;
cluster Upper_Arc a1 -> with_the_max_arc ;
coherence
Upper_Arc c1 is with_the_max_arc
proof end;
end;

theorem Th70: :: JORDAN21:70
for b1 being Simple_closed_curve
for b2 being Nat holds UMP (Upper_Arc (L~ (Cage b1,b2))) in Upper_Arc (L~ (Cage b1,b2)) by Th43;

theorem Th71: :: JORDAN21:71
for b1 being Simple_closed_curve
for b2 being Nat holds LMP (Lower_Arc (L~ (Cage b1,b2))) in Lower_Arc (L~ (Cage b1,b2)) by Th44;

theorem Th72: :: JORDAN21:72
for b1 being Simple_closed_curve
for b2 being Nat st 0 < b2 holds
ex b3 being Nat st
( 1 <= b3 & b3 <= len (Gauge b1,b2) & UMP (L~ (Cage b1,b2)) = (Gauge b1,b2) * (Center (Gauge b1,b2)),b3 )
proof end;

theorem Th73: :: JORDAN21:73
for b1 being Simple_closed_curve
for b2 being Nat st 0 < b2 holds
ex b3 being Nat st
( 1 <= b3 & b3 <= len (Gauge b1,b2) & LMP (L~ (Cage b1,b2)) = (Gauge b1,b2) * (Center (Gauge b1,b2)),b3 )
proof end;

theorem Th74: :: JORDAN21:74
for b1 being Simple_closed_curve
for b2 being Nat st 0 < b2 holds
UMP (L~ (Cage b1,b2)) = UMP (Upper_Arc (L~ (Cage b1,b2)))
proof end;

theorem Th75: :: JORDAN21:75
for b1 being Simple_closed_curve
for b2 being Nat st 0 < b2 holds
LMP (L~ (Cage b1,b2)) = LMP (Lower_Arc (L~ (Cage b1,b2)))
proof end;

theorem Th76: :: JORDAN21:76
for b1 being Simple_closed_curve
for b2 being Nat st 0 < b2 holds
(UMP b1) `2 < (UMP (Upper_Arc (L~ (Cage b1,b2)))) `2
proof end;

theorem Th77: :: JORDAN21:77
for b1 being Simple_closed_curve
for b2 being Nat st 0 < b2 holds
(LMP (Lower_Arc (L~ (Cage b1,b2)))) `2 < (LMP b1) `2
proof end;

theorem Th78: :: JORDAN21:78
for b1 being Simple_closed_curve
for b2, b3 being Nat st b2 <= b3 holds
(UMP (L~ (Cage b1,b3))) `2 <= (UMP (L~ (Cage b1,b2))) `2
proof end;

theorem Th79: :: JORDAN21:79
for b1 being Simple_closed_curve
for b2, b3 being Nat st b2 <= b3 holds
(LMP (L~ (Cage b1,b2))) `2 <= (LMP (L~ (Cage b1,b3))) `2
proof end;

theorem Th80: :: JORDAN21:80
for b1 being Simple_closed_curve
for b2, b3 being Nat st 0 < b2 & b2 <= b3 holds
(UMP (Upper_Arc (L~ (Cage b1,b3)))) `2 <= (UMP (Upper_Arc (L~ (Cage b1,b2)))) `2
proof end;

theorem Th81: :: JORDAN21:81
for b1 being Simple_closed_curve
for b2, b3 being Nat st 0 < b2 & b2 <= b3 holds
(LMP (Lower_Arc (L~ (Cage b1,b2)))) `2 <= (LMP (Lower_Arc (L~ (Cage b1,b3)))) `2
proof end;