let n be Nat; :: thesis: for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
let C be Simple_closed_curve; :: thesis: for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
let i1, i2, j, k be Nat; :: thesis: ( 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Lower_Arc (L~ (Cage (C,(n + 1)))) implies (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C )
set G = Gauge (C,(n + 1));
assume that
A1: 1 < i1 and
A2: i1 < len (Gauge (C,(n + 1))) and
A3: 1 < i2 and
A4: i2 < len (Gauge (C,(n + 1))) and
A5: 1 <= j and
A6: j <= k and
A7: k <= width (Gauge (C,(n + 1))) and
A8: (Gauge (C,(n + 1))) * (i1,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) and
A9: (Gauge (C,(n + 1))) * (i2,j) in Lower_Arc (L~ (Cage (C,(n + 1)))) ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
A10: 1 <= k by A5, A6, XXREAL_0:2;
then A11: [i2,k] in Indices (Gauge (C,(n + 1))) by A3, A4, A7, MATRIX_0:30;
A12: [i1,k] in Indices (Gauge (C,(n + 1))) by A1, A2, A7, A10, MATRIX_0:30;
((Gauge (C,(n + 1))) * (i2,k)) `2 = ((Gauge (C,(n + 1))) * (1,k)) `2 by A3, A4, A7, A10, GOBOARD5:1
.= ((Gauge (C,(n + 1))) * (i1,k)) `2 by A1, A2, A7, A10, GOBOARD5:1 ;
then A13: LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) is horizontal by SPPOL_1:15;
A14: Lower_Arc (L~ (Cage (C,(n + 1)))) = L~ (Lower_Seq (C,(n + 1))) by JORDAN1G:56;
A15: j <= width (Gauge (C,(n + 1))) by A6, A7, XXREAL_0:2;
then A16: [i2,j] in Indices (Gauge (C,(n + 1))) by A3, A4, A5, MATRIX_0:30;
((Gauge (C,(n + 1))) * (i2,j)) `1 = ((Gauge (C,(n + 1))) * (i2,1)) `1 by A3, A4, A5, A15, GOBOARD5:2
.= ((Gauge (C,(n + 1))) * (i2,k)) `1 by A3, A4, A7, A10, GOBOARD5:2 ;
then A17: LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) is vertical by SPPOL_1:16;
A18: Upper_Arc (L~ (Cage (C,(n + 1)))) = L~ (Upper_Seq (C,(n + 1))) by JORDAN1G:55;
A19: [i2,k] in Indices (Gauge (C,(n + 1))) by A3, A4, A7, A10, MATRIX_0:30;
now :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
per cases ( LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) meets Upper_Arc (L~ (Cage (C,(n + 1)))) or ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Lower_Arc (L~ (Cage (C,(n + 1)))) & i2 <= i1 ) or ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Lower_Arc (L~ (Cage (C,(n + 1)))) & i1 < i2 ) or ( LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) misses Upper_Arc (L~ (Cage (C,(n + 1)))) & LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) misses Lower_Arc (L~ (Cage (C,(n + 1)))) ) ) ;
suppose A20: LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) meets Upper_Arc (L~ (Cage (C,(n + 1)))) ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
set X = (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))));
ex x being object st
( x in LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) & x in L~ (Upper_Seq (C,(n + 1))) ) by A18, A20, XBOOLE_0:3;
then reconsider X1 = (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) as non empty compact Subset of (TOP-REAL 2) by XBOOLE_0:def 4;
consider pp being object such that
A21: pp in S-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A21;
A22: pp in (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) by A21, XBOOLE_0:def 4;
then A23: pp in L~ (Upper_Seq (C,(n + 1))) by XBOOLE_0:def 4;
A24: pp in LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) by A22, XBOOLE_0:def 4;
consider m being Nat such that
A25: j <= m and
A26: m <= k and
A27: ((Gauge (C,(n + 1))) * (i2,m)) `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))) by A6, A18, A16, A19, A20, JORDAN1F:1, JORDAN1G:4;
A28: m <= width (Gauge (C,(n + 1))) by A7, A26, XXREAL_0:2;
1 <= m by A5, A25, XXREAL_0:2;
then A29: ((Gauge (C,(n + 1))) * (i2,m)) `1 = ((Gauge (C,(n + 1))) * (i2,1)) `1 by A3, A4, A28, GOBOARD5:2;
then A30: |[(((Gauge (C,(n + 1))) * (i2,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))))]| = (Gauge (C,(n + 1))) * (i2,m) by A27, EUCLID:53;
then ((Gauge (C,(n + 1))) * (i2,j)) `1 = |[(((Gauge (C,(n + 1))) * (i2,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))))]| `1 by A3, A4, A5, A15, A29, GOBOARD5:2;
then A31: pp `1 = |[(((Gauge (C,(n + 1))) * (i2,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))))]| `1 by A17, A24, SPPOL_1:41;
|[(((Gauge (C,(n + 1))) * (i2,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))))]| `2 = S-bound ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))) by A27, A30, SPRECT_1:44
.= (S-min ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))) `2 by EUCLID:52
.= pp `2 by A21, PSCOMP_1:55 ;
then (Gauge (C,(n + 1))) * (i2,m) in Upper_Arc (L~ (Cage (C,(n + 1)))) by A18, A30, A23, A31, TOPREAL3:6;
then LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,m))) meets Upper_Arc C by A3, A4, A5, A9, A25, A28, Th24;
then LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) meets Upper_Arc C by A3, A4, A5, A7, A25, A26, Th5, XBOOLE_1:63;
hence (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C by XBOOLE_1:70; :: thesis: verum
end;
suppose A32: ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Lower_Arc (L~ (Cage (C,(n + 1)))) & i2 <= i1 ) ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
set X = (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1))));
ex x being object st
( x in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) & x in L~ (Lower_Seq (C,(n + 1))) ) by A14, A32, XBOOLE_0:3;
then reconsider X1 = (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) as non empty compact Subset of (TOP-REAL 2) by XBOOLE_0:def 4;
consider pp being object such that
A33: pp in E-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A33;
A34: pp in (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) by A33, XBOOLE_0:def 4;
then A35: pp in L~ (Lower_Seq (C,(n + 1))) by XBOOLE_0:def 4;
A36: pp in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) by A34, XBOOLE_0:def 4;
consider m being Nat such that
A37: i2 <= m and
A38: m <= i1 and
A39: ((Gauge (C,(n + 1))) * (m,k)) `1 = upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))) by A14, A11, A12, A32, JORDAN1F:4, JORDAN1G:5;
A40: 1 < m by A3, A37, XXREAL_0:2;
m < len (Gauge (C,(n + 1))) by A2, A38, XXREAL_0:2;
then A41: ((Gauge (C,(n + 1))) * (m,k)) `2 = ((Gauge (C,(n + 1))) * (1,k)) `2 by A7, A10, A40, GOBOARD5:1;
then A42: |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| = (Gauge (C,(n + 1))) * (m,k) by A39, EUCLID:53;
then ((Gauge (C,(n + 1))) * (i2,k)) `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `2 by A3, A4, A7, A10, A41, GOBOARD5:1;
then A43: pp `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `2 by A13, A36, SPPOL_1:40;
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `1 = E-bound ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))) by A39, A42, SPRECT_1:46
.= (E-min ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))) `1 by EUCLID:52
.= pp `1 by A33, PSCOMP_1:47 ;
then (Gauge (C,(n + 1))) * (m,k) in Lower_Arc (L~ (Cage (C,(n + 1)))) by A14, A42, A35, A43, TOPREAL3:6;
then LSeg (((Gauge (C,(n + 1))) * (m,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Upper_Arc C by A2, A7, A8, A10, A38, A40, Th33;
then LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Upper_Arc C by A2, A3, A7, A10, A37, A38, Th6, XBOOLE_1:63;
hence (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C by XBOOLE_1:70; :: thesis: verum
end;
suppose A44: ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Lower_Arc (L~ (Cage (C,(n + 1)))) & i1 < i2 ) ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
set X = (LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1))));
ex x being object st
( x in LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k))) & x in L~ (Lower_Seq (C,(n + 1))) ) by A14, A44, XBOOLE_0:3;
then reconsider X1 = (LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) as non empty compact Subset of (TOP-REAL 2) by XBOOLE_0:def 4;
consider pp being object such that
A45: pp in W-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A45;
A46: pp in (LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) by A45, XBOOLE_0:def 4;
then A47: pp in L~ (Lower_Seq (C,(n + 1))) by XBOOLE_0:def 4;
A48: pp in LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k))) by A46, XBOOLE_0:def 4;
consider m being Nat such that
A49: i1 <= m and
A50: m <= i2 and
A51: ((Gauge (C,(n + 1))) * (m,k)) `1 = lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))) by A14, A11, A12, A44, JORDAN1F:3, JORDAN1G:5;
A52: m < len (Gauge (C,(n + 1))) by A4, A50, XXREAL_0:2;
1 < m by A1, A49, XXREAL_0:2;
then A53: ((Gauge (C,(n + 1))) * (m,k)) `2 = ((Gauge (C,(n + 1))) * (1,k)) `2 by A7, A10, A52, GOBOARD5:1;
then A54: |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| = (Gauge (C,(n + 1))) * (m,k) by A51, EUCLID:53;
then ((Gauge (C,(n + 1))) * (i1,k)) `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `2 by A1, A2, A7, A10, A53, GOBOARD5:1;
then A55: pp `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `2 by A13, A48, SPPOL_1:40;
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `1 = W-bound ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))) by A51, A54, SPRECT_1:43
.= (W-min ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))) `1 by EUCLID:52
.= pp `1 by A45, PSCOMP_1:31 ;
then (Gauge (C,(n + 1))) * (m,k) in Lower_Arc (L~ (Cage (C,(n + 1)))) by A14, A54, A47, A55, TOPREAL3:6;
then LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (m,k))) meets Upper_Arc C by A1, A7, A8, A10, A49, A52, Th41;
then LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k))) meets Upper_Arc C by A1, A4, A7, A10, A49, A50, Th6, XBOOLE_1:63;
hence (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C by XBOOLE_1:70; :: thesis: verum
end;
suppose A56: ( LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) misses Upper_Arc (L~ (Cage (C,(n + 1)))) & LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) misses Lower_Arc (L~ (Cage (C,(n + 1)))) ) ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
consider j1 being Nat such that
A57: j <= j1 and
A58: j1 <= k and
A59: (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i2,j1))} by A3, A4, A5, A6, A7, A9, A14, Th9;
(Gauge (C,(n + 1))) * (i2,j1) in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) by A59, TARSKI:def 1;
then A60: (Gauge (C,(n + 1))) * (i2,j1) in L~ (Lower_Seq (C,(n + 1))) by XBOOLE_0:def 4;
A61: 1 <= j1 by A5, A57, XXREAL_0:2;
now :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
per cases ( i2 <= i1 or i1 < i2 ) ;
suppose A62: i2 <= i1 ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
A63: LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) c= LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) by A3, A4, A5, A7, A57, A58, Th5;
consider i3 being Nat such that
A64: i2 <= i3 and
A65: i3 <= i1 and
A66: (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))} by A2, A3, A7, A8, A18, A10, A62, Th13;
A67: LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) c= LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) by A2, A3, A7, A10, A64, A65, Th6;
then A68: (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) c= (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) by A63, XBOOLE_1:13;
(Gauge (C,(n + 1))) * (i3,k) in (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) by A66, TARSKI:def 1;
then A69: (Gauge (C,(n + 1))) * (i3,k) in L~ (Upper_Seq (C,(n + 1))) by XBOOLE_0:def 4;
A70: ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))}
proof
thus ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) c= {((Gauge (C,(n + 1))) * (i3,k))} :: according to XBOOLE_0:def 10 :: thesis: {((Gauge (C,(n + 1))) * (i3,k))} c= ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) or x in {((Gauge (C,(n + 1))) * (i3,k))} )
assume A71: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) ; :: thesis: x in {((Gauge (C,(n + 1))) * (i3,k))}
then x in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 4;
then A72: ( x in LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) or x in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) ) by XBOOLE_0:def 3;
x in L~ (Upper_Seq (C,(n + 1))) by A71, XBOOLE_0:def 4;
hence x in {((Gauge (C,(n + 1))) * (i3,k))} by A18, A56, A66, A63, A72, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,(n + 1))) * (i3,k))} or x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) )
(Gauge (C,(n + 1))) * (i3,k) in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) by RLTOPSP1:68;
then A73: (Gauge (C,(n + 1))) * (i3,k) in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 3;
assume x in {((Gauge (C,(n + 1))) * (i3,k))} ; :: thesis: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
then x = (Gauge (C,(n + 1))) * (i3,k) by TARSKI:def 1;
hence x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) by A69, A73, XBOOLE_0:def 4; :: thesis: verum
end;
A74: ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i2,j1))}
proof
thus ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) c= {((Gauge (C,(n + 1))) * (i2,j1))} :: according to XBOOLE_0:def 10 :: thesis: {((Gauge (C,(n + 1))) * (i2,j1))} c= ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) or x in {((Gauge (C,(n + 1))) * (i2,j1))} )
assume A75: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) ; :: thesis: x in {((Gauge (C,(n + 1))) * (i2,j1))}
then x in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 4;
then A76: ( x in LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) or x in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) ) by XBOOLE_0:def 3;
x in L~ (Lower_Seq (C,(n + 1))) by A75, XBOOLE_0:def 4;
hence x in {((Gauge (C,(n + 1))) * (i2,j1))} by A14, A56, A59, A67, A76, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,(n + 1))) * (i2,j1))} or x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) )
(Gauge (C,(n + 1))) * (i2,j1) in LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) by RLTOPSP1:68;
then A77: (Gauge (C,(n + 1))) * (i2,j1) in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 3;
assume x in {((Gauge (C,(n + 1))) * (i2,j1))} ; :: thesis: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
then x = (Gauge (C,(n + 1))) * (i2,j1) by TARSKI:def 1;
hence x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) by A60, A77, XBOOLE_0:def 4; :: thesis: verum
end;
i3 < len (Gauge (C,(n + 1))) by A2, A65, XXREAL_0:2;
hence (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C by A3, A7, A58, A61, A64, A68, A70, A74, Th44, XBOOLE_1:63; :: thesis: verum
end;
suppose A78: i1 < i2 ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
A79: LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) c= LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) by A3, A4, A5, A7, A57, A58, Th5;
consider i3 being Nat such that
A80: i1 <= i3 and
A81: i3 <= i2 and
A82: (LSeg (((Gauge (C,(n + 1))) * (i3,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))} by A1, A4, A7, A8, A18, A10, A78, Th18;
A83: LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) c= LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) by A1, A4, A7, A10, A80, A81, Th6;
then A84: (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) c= (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) by A79, XBOOLE_1:13;
(Gauge (C,(n + 1))) * (i3,k) in (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) by A82, TARSKI:def 1;
then A85: (Gauge (C,(n + 1))) * (i3,k) in L~ (Upper_Seq (C,(n + 1))) by XBOOLE_0:def 4;
A86: ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))}
proof
thus ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) c= {((Gauge (C,(n + 1))) * (i3,k))} :: according to XBOOLE_0:def 10 :: thesis: {((Gauge (C,(n + 1))) * (i3,k))} c= ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) or x in {((Gauge (C,(n + 1))) * (i3,k))} )
assume A87: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) ; :: thesis: x in {((Gauge (C,(n + 1))) * (i3,k))}
then x in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 4;
then A88: ( x in LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) or x in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) ) by XBOOLE_0:def 3;
x in L~ (Upper_Seq (C,(n + 1))) by A87, XBOOLE_0:def 4;
hence x in {((Gauge (C,(n + 1))) * (i3,k))} by A18, A56, A82, A79, A88, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,(n + 1))) * (i3,k))} or x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) )
(Gauge (C,(n + 1))) * (i3,k) in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) by RLTOPSP1:68;
then A89: (Gauge (C,(n + 1))) * (i3,k) in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 3;
assume x in {((Gauge (C,(n + 1))) * (i3,k))} ; :: thesis: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
then x = (Gauge (C,(n + 1))) * (i3,k) by TARSKI:def 1;
hence x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) by A85, A89, XBOOLE_0:def 4; :: thesis: verum
end;
A90: ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i2,j1))}
proof
thus ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) c= {((Gauge (C,(n + 1))) * (i2,j1))} :: according to XBOOLE_0:def 10 :: thesis: {((Gauge (C,(n + 1))) * (i2,j1))} c= ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) or x in {((Gauge (C,(n + 1))) * (i2,j1))} )
assume A91: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) ; :: thesis: x in {((Gauge (C,(n + 1))) * (i2,j1))}
then x in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 4;
then A92: ( x in LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) or x in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) ) by XBOOLE_0:def 3;
x in L~ (Lower_Seq (C,(n + 1))) by A91, XBOOLE_0:def 4;
hence x in {((Gauge (C,(n + 1))) * (i2,j1))} by A14, A56, A59, A83, A92, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,(n + 1))) * (i2,j1))} or x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) )
(Gauge (C,(n + 1))) * (i2,j1) in LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) by RLTOPSP1:68;
then A93: (Gauge (C,(n + 1))) * (i2,j1) in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 3;
assume x in {((Gauge (C,(n + 1))) * (i2,j1))} ; :: thesis: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
then x = (Gauge (C,(n + 1))) * (i2,j1) by TARSKI:def 1;
hence x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) by A60, A93, XBOOLE_0:def 4; :: thesis: verum
end;
1 < i3 by A1, A80, XXREAL_0:2;
hence (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C by A4, A7, A58, A61, A81, A84, A86, A90, Th46, XBOOLE_1:63; :: thesis: verum
end;
end;
end;
hence (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C ; :: thesis: verum
end;
end;
end;
hence (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C ; :: thesis: verum