let C be Simple_closed_curve; for n being Nat st 0 < n holds
upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))
let n be Nat; ( 0 < n implies upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))) )
set f = Cage (C,n);
set G = Gauge (C,n);
set c = Center (Gauge (C,n));
set Y = proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)));
set X = proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))));
A1:
len (Gauge (C,n)) = width (Gauge (C,n))
by JORDAN8:def 1;
A2:
1 <= len (Gauge (C,n))
by Lm3;
assume
0 < n
; upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))
then A3: ((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 =
((W-bound C) + (E-bound C)) / 2
by A1, A2, JORDAN1G:35
.=
((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by JORDAN1G:33
;
then A4:
(Gauge (C,n)) * ((Center (Gauge (C,n))),1) in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)
;
A5:
proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) is bounded_above
by JORDAN21:13;
LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n)))
by JORDAN1B:31;
then
LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets L~ (Cage (C,n))
by JORDAN6:61, XBOOLE_1:63;
then A6:
not (L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) is empty
by XBOOLE_0:def 7;
then A7:
not proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) is empty
by Lm2, RELAT_1:119;
A8:
Center (Gauge (C,n)) <= len (Gauge (C,n))
by JORDAN1B:13;
1 <= Center (Gauge (C,n))
by JORDAN1B:11;
then A9:
((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `1
by A1, A2, A8, GOBOARD5:2;
then
(Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))) in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)
by A3;
then A10:
((L~ (Cage (C,n))) /\ (L~ (Cage (C,n)))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))) c= (L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))
by A4, JORDAN1A:13, XBOOLE_1:26;
then A11:
proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) c= proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))
by RELAT_1:123;
then A12:
for r being Real st r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) holds
r <= upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))
by A5, SEQ_4:def 1;
A13:
not proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))) is empty
by A11, A6, Lm2, RELAT_1:119, XBOOLE_1:3;
A14:
for s being Real st 0 < s holds
ex r being Real st
( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r )
proof
let s be
Real;
( 0 < s implies ex r being Real st
( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r ) )
assume
0 < s
;
ex r being Real st
( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r )
then consider r being
Real such that A15:
r in proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)))
and A16:
(upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r
by A5, A13, SEQ_4:def 1;
take
r
;
( r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) & (upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r )
consider x being
Point of
(TOP-REAL 2) such that A17:
x in (L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))
and A18:
proj2 . x = r
by A15, Lm1;
A19:
x in L~ (Cage (C,n))
by A17, XBOOLE_0:def 4;
x in Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2)
by A17, XBOOLE_0:def 4;
then A20:
((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `1 = x `1
by A3, JORDAN6:31;
A21:
GoB (Cage (C,n)) = Gauge (
C,
n)
by JORDAN1H:44;
then A22:
((Gauge (C,n)) * ((Center (Gauge (C,n))),1)) `2 <= x `2
by A8, A19, JORDAN1B:11, JORDAN5D:33;
x `2 <= ((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))) `2
by A1, A8, A19, A21, JORDAN1B:11, JORDAN5D:34;
then
x in LSeg (
((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),
((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))
by A9, A20, A22, GOBOARD7:7;
then
x in (L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))
by A19, XBOOLE_0:def 4;
hence
r in proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))
by A18, FUNCT_2:35;
(upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r
thus
(upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))) - s < r
by A16;
verum
end;
proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))))) is bounded_above
by A10, A5, RELAT_1:123, XXREAL_2:43;
hence
upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))
by A7, A12, A14, SEQ_4:def 1; verum