let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j being Nat st (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) & 1 <= j & j <= width (Gauge (C,(n + 1))) holds
LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) meets Upper_Arc (L~ (Cage (C,(n + 1))))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for j being Nat st (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) & 1 <= j & j <= width (Gauge (C,(n + 1))) holds
LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) meets Upper_Arc (L~ (Cage (C,(n + 1))))
let j be Nat; ( (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) & 1 <= j & j <= width (Gauge (C,(n + 1))) implies LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) meets Upper_Arc (L~ (Cage (C,(n + 1)))) )
assume that
A1:
(Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1))))
and
A2:
1 <= j
and
A3:
j <= width (Gauge (C,(n + 1)))
; LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) meets Upper_Arc (L~ (Cage (C,(n + 1))))
set in1 = Center (Gauge (C,(n + 1)));
A4:
n + 1 >= 0 + 1
by NAT_1:11;
A5:
1 <= Center (Gauge (C,(n + 1)))
by JORDAN1B:11;
A6:
Center (Gauge (C,(n + 1))) <= len (Gauge (C,(n + 1)))
by JORDAN1B:13;
A7:
LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),(width (Gauge (C,(n + 1)))))),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) c= LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)))
by A2, A3, A4, Th2;
Lower_Arc (L~ (Cage (C,(n + 1)))) c= L~ (Cage (C,(n + 1)))
by JORDAN6:61;
hence
LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j))) meets Upper_Arc (L~ (Cage (C,(n + 1))))
by A1, A2, A3, A5, A6, A7, Th4, XBOOLE_1:63; verum