let C be Simple_closed_curve; :: thesis:
let n be Element of NAT ; :: thesis:
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 ; :: thesis:
then A3: ((Gauge C,n) * (Center (Gauge C,n)),1) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, A2, JORDAN1G:43
.= ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2 by JORDAN1G:41 ;
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:34;
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:76, 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:152;
A8: Center (Gauge C,n) <= len (Gauge C,n) by JORDAN1B:14;
1 <= Center (Gauge C,n) by JORDAN1B:12;
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:3;
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:23, 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:156;
then A12: for r being real number 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 4;
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:152, XBOOLE_1:3;
A14: for s being real number st 0 < s holds
ex r being real number 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 )

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider r being real number 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 4;
take r ; :: thesis:
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:34;
A21: GoB (Cage C,n) = Gauge C,n by JORDAN1H:52;
then A22: ((Gauge C,n) * (Center (Gauge C,n)),1) `2 <= x `2 by A8, A19, JORDAN1B:12, JORDAN5D:35;
x `2 <= ((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) `2 by A1, A8, A19, A21, JORDAN1B:12, JORDAN5D:36;
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:8;
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:43; :: thesis:
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; :: thesis:

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:156, 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 4; :: thesis: