let C be Simple_closed_curve; :: thesis:
let n be Element of NAT ; :: thesis:
assume A1: 0 < n ; :: 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)))));
A2: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A3: 1 <= len (Gauge C,n) by Lm3;
A4: ( 1 <= Center (Gauge C,n) & Center (Gauge C,n) <= len (Gauge C,n) ) by JORDAN1B:12, JORDAN1B:14;
then A5: ((Gauge C,n) * (Center (Gauge C,n)),1) `1 = ((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) `1 by A2, A3, GOBOARD5:3;
A6: ((Gauge C,n) * (Center (Gauge C,n)),1) `1 = ((W-bound C) + (E-bound C)) / 2 by A1, A2, A3, JORDAN1G:43
.= ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2 by JORDAN1G:41 ;
then ( (Gauge C,n) * (Center (Gauge C,n)),1 in Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2) & (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 A5;
then A7: ((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 JORDAN1A:23, XBOOLE_1:26;
then A8: 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;
A9: proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2))) is bounded_below by JORDAN21:13;
then A10: 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_below by A7, RELAT_1:156, XXREAL_2:44;
A11: 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;
Upper_Arc (L~ (Cage C,n)) c= L~ (Cage C,n) by JORDAN6:76;
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 A11, XBOOLE_1:63;
then A12: 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 A13: 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;
A14: not proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2))) is empty by A8, A12, Lm2, RELAT_1:152, XBOOLE_1:3;
A15: 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
inf (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2)))) <= r by A8, A9, SEQ_4:def 5;
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))))) & r < (lower_bound (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2))))) + s )

proof

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider r being real number such that
A16: r in proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2))) and
A17: r < (lower_bound (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2))))) + s by A9, A14, SEQ_4:def 5;
take r ; :: thesis:
consider x being Point of (TOP-REAL 2) such that
A18: x in (L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2)) and
A19: proj2 . x = r by A16, Lm1;
A20: x in L~ (Cage C,n) by A18, XBOOLE_0:def 4;
x in Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2) by A18, XBOOLE_0:def 4;
then A21: ((Gauge C,n) * (Center (Gauge C,n)),1) `1 = x `1 by A6, JORDAN6:34;
GoB (Cage C,n) = Gauge C,n by JORDAN1H:52;
then ( ((Gauge C,n) * (Center (Gauge C,n)),1) `2 <= x `2 & x `2 <= ((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) `2 ) by A2, A4, A20, JORDAN5D:35, 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 A5, A21, 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 A20, 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 A19, FUNCT_2:43; :: thesis:
thus r < (lower_bound (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2))))) + s by A17; :: thesis:

end;

hence inf (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)))))) = inf (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2)))) by A10, A13, A15, SEQ_4:def 5; :: thesis: