let C be Simple_closed_curve; :: thesis:
let n be 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: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; :: thesis:
assume 0 < s ; :: thesis:
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 ; :: 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: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; :: 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: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; :: thesis: