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 Lower_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Upper_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 Lower_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 Lower_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Upper_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 Lower_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 Lower_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Upper_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 Lower_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 Lower_Arc (L~ (Cage (C,(n + 1)))) and
A9: (Gauge (C,(n + 1))) * (i2,j) in 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 Lower_Arc C
A10: Lower_Arc (L~ (Cage (C,(n + 1)))) = L~ (Lower_Seq (C,(n + 1))) by JORDAN1G:56;
A11: Upper_Arc (L~ (Cage (C,(n + 1)))) = L~ (Upper_Seq (C,(n + 1))) by JORDAN1G:55;
A12: j <= width (Gauge (C,(n + 1))) by A6, A7, XXREAL_0:2;
then A13: [i2,j] in Indices (Gauge (C,(n + 1))) by A3, A4, A5, MATRIX_0:30;
A14: 1 <= k by A5, A6, XXREAL_0:2;
then A15: [i2,k] in Indices (Gauge (C,(n + 1))) by A3, A4, A7, MATRIX_0:30;
((Gauge (C,(n + 1))) * (i2,j)) `1 = ((Gauge (C,(n + 1))) * (i2,1)) `1 by A3, A4, A5, A12, GOBOARD5:2
.= ((Gauge (C,(n + 1))) * (i2,k)) `1 by A3, A4, A7, A14, GOBOARD5:2 ;
then A16: LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) is vertical by SPPOL_1:16;
((Gauge (C,(n + 1))) * (i2,k)) `2 = ((Gauge (C,(n + 1))) * (1,k)) `2 by A3, A4, A7, A14, GOBOARD5:1
.= ((Gauge (C,(n + 1))) * (i1,k)) `2 by A1, A2, A7, A14, GOBOARD5:1 ;
then A17: LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) is horizontal by SPPOL_1:15;
A18: [i2,k] in Indices (Gauge (C,(n + 1))) by A3, A4, A7, A14, MATRIX_0:30;
A19: [i1,k] in Indices (Gauge (C,(n + 1))) by A1, A2, A7, A14, 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 Lower_Arc C

per cases ( LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) meets Lower_Arc (L~ (Cage (C,(n + 1)))) or ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Upper_Arc (L~ (Cage (C,(n + 1)))) & i2 <= i1 ) or ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Upper_Arc (L~ (Cage (C,(n + 1)))) & i1 < i2 ) or ( LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) misses Lower_Arc (L~ (Cage (C,(n + 1)))) & LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) misses Upper_Arc (L~ (Cage (C,(n + 1)))) ) ) ;

suppose A20: LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) meets 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 Lower_Arc C

then consider m being Nat such that
A21: j <= m and
A22: m <= k and
A23: ((Gauge (C,(n + 1))) * (i2,m)) `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))) by A6, A10, A13, A15, JORDAN1F:1, JORDAN1G:5;
A24: 1 <= m by A5, A21, XXREAL_0:2;
A25: m <= width (Gauge (C,(n + 1))) by A7, A22, XXREAL_0:2;
set X = (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1))));
((Gauge (C,(n + 1))) * (i2,m)) `1 = ((Gauge (C,(n + 1))) * (i2,1)) `1 by A3, A4, A24, A25, GOBOARD5:2;
then A27: |[(((Gauge (C,(n + 1))) * (i2,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))))]| = (Gauge (C,(n + 1))) * (i2,m) by A23, EUCLID:53;
A28: ((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~ (Lower_Seq (C,(n + 1)))))))]| `1 by A3, A4, A5, A12, GOBOARD5:2;
ex x being object st
( x in LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) & x in L~ (Lower_Seq (C,(n + 1))) ) by A10, A20, XBOOLE_0:3;
then reconsider X1 = (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((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
A29: pp in S-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A29;
A30: pp in (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) by A29, XBOOLE_0:def 4;
then A31: pp in L~ (Lower_Seq (C,(n + 1))) by XBOOLE_0:def 4;
pp in LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) by A30, XBOOLE_0:def 4;
then A32: 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~ (Lower_Seq (C,(n + 1)))))))]| `1 by A16, A28, 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~ (Lower_Seq (C,(n + 1)))))))]| `2 = S-bound ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))) by SPRECT_1:44
.= (S-min ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))) `2
.= pp `2 by A29, PSCOMP_1:55 ;
then (Gauge (C,(n + 1))) * (i2,m) in Lower_Arc (L~ (Cage (C,(n + 1)))) by A10, A27, A31, A32, TOPREAL3:6;
then LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,m))) meets Lower_Arc C by A3, A4, A5, A9, A21, A25, Th19;
then LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) meets Lower_Arc C by A3, A4, A5, A7, A21, A22, JORDAN15:5, 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 Lower_Arc C by XBOOLE_1:70; :: thesis: verum

end;

suppose A33: ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Upper_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 Lower_Arc C

then consider m being Nat such that
A34: i2 <= m and
A35: m <= i1 and
A36: ((Gauge (C,(n + 1))) * (m,k)) `1 = upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))) by A11, A18, A19, JORDAN1F:4, JORDAN1G:4;
A37: 1 < m by A3, A34, XXREAL_0:2;
A38: m < len (Gauge (C,(n + 1))) by A2, A35, XXREAL_0:2;
set X = (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1))));
((Gauge (C,(n + 1))) * (m,k)) `2 = ((Gauge (C,(n + 1))) * (1,k)) `2 by A7, A14, A37, A38, GOBOARD5:1;
then A40: |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| = (Gauge (C,(n + 1))) * (m,k) by A36, EUCLID:53;
A41: ((Gauge (C,(n + 1))) * (i2,k)) `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `2 by A3, A4, A7, A14, GOBOARD5:1;
ex x being object st
( x in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) & x in L~ (Upper_Seq (C,(n + 1))) ) by A11, A33, XBOOLE_0:3;
then reconsider X1 = (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,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
A42: pp in E-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A42;
A43: pp in (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) by A42, XBOOLE_0:def 4;
then A44: pp in L~ (Upper_Seq (C,(n + 1))) by XBOOLE_0:def 4;
pp in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) by A43, XBOOLE_0:def 4;
then A45: pp `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `2 by A17, A41, SPPOL_1:40;
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_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~ (Upper_Seq (C,(n + 1))))) by SPRECT_1:46
.= (E-min ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))) `1
.= pp `1 by A42, PSCOMP_1:47 ;
then (Gauge (C,(n + 1))) * (m,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) by A11, A40, A44, A45, TOPREAL3:6;
then LSeg (((Gauge (C,(n + 1))) * (m,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Lower_Arc C by A2, A7, A8, A14, A35, A37, JORDAN15:40;
then LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Lower_Arc C by A2, A3, A7, A14, A34, A35, JORDAN15:6, 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 Lower_Arc C by XBOOLE_1:70; :: thesis: verum

end;

suppose A46: ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Upper_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 Lower_Arc C

then consider m being Nat such that
A47: i1 <= m and
A48: m <= i2 and
A49: ((Gauge (C,(n + 1))) * (m,k)) `1 = lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))) by A11, A18, A19, JORDAN1F:3, JORDAN1G:4;
A50: 1 < m by A1, A47, XXREAL_0:2;
A51: m < len (Gauge (C,(n + 1))) by A4, A48, XXREAL_0:2;
set X = (LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))));
((Gauge (C,(n + 1))) * (m,k)) `2 = ((Gauge (C,(n + 1))) * (1,k)) `2 by A7, A14, A50, A51, GOBOARD5:1;
then A53: |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| = (Gauge (C,(n + 1))) * (m,k) by A49, EUCLID:53;
A54: ((Gauge (C,(n + 1))) * (i1,k)) `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `2 by A1, A2, A7, A14, GOBOARD5:1;
ex x being object st
( x in LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k))) & x in L~ (Upper_Seq (C,(n + 1))) ) by A11, A46, XBOOLE_0:3;
then reconsider X1 = (LSeg (((Gauge (C,(n + 1))) * (i1,k)),((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
A55: pp in W-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A55;
A56: pp in (LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) by A55, XBOOLE_0:def 4;
then A57: pp in L~ (Upper_Seq (C,(n + 1))) by XBOOLE_0:def 4;
pp in LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k))) by A56, XBOOLE_0:def 4;
then A58: pp `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `2 by A17, A54, SPPOL_1:40;
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_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~ (Upper_Seq (C,(n + 1))))) by SPRECT_1:43
.= (W-min ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))) `1
.= pp `1 by A55, PSCOMP_1:31 ;
then (Gauge (C,(n + 1))) * (m,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) by A11, A53, A57, A58, TOPREAL3:6;
then LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (m,k))) meets Lower_Arc C by A1, A7, A8, A14, A47, A51, JORDAN15:32;
then LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k))) meets Lower_Arc C by A1, A4, A7, A14, A47, A48, JORDAN15:6, 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 Lower_Arc C by XBOOLE_1:70; :: thesis: verum

end;

suppose A59: ( LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) misses Lower_Arc (L~ (Cage (C,(n + 1)))) & LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) misses 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 Lower_Arc C

consider j1 being Nat such that
A60: j <= j1 and
A61: j1 <= k and
A62: (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i2,j1))} by A3, A4, A5, A6, A7, A9, A11, JORDAN15:15;
(Gauge (C,(n + 1))) * (i2,j1) in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) by A62, TARSKI:def 1;
then A63: (Gauge (C,(n + 1))) * (i2,j1) in L~ (Upper_Seq (C,(n + 1))) by XBOOLE_0:def 4;
A64: 1 <= j1 by A5, A60, 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 Lower_Arc C

per cases ( i2 <= i1 or i1 < i2 ) ;

suppose 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 Lower_Arc C

then consider i3 being Nat such that
A65: i2 <= i3 and
A66: i3 <= i1 and
A67: (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))} by A2, A3, A7, A8, A10, A14, JORDAN15:19;
A68: i3 < len (Gauge (C,(n + 1))) by A2, A66, XXREAL_0:2;
(Gauge (C,(n + 1))) * (i3,k) in (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) by A67, TARSKI:def 1;
then A69: (Gauge (C,(n + 1))) * (i3,k) in L~ (Lower_Seq (C,(n + 1))) by XBOOLE_0:def 4;
A70: 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, A60, A61, JORDAN15:5;
A71: 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, A14, A65, A66, JORDAN15:6;
then A72: (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 A70, XBOOLE_1:13;
A73: ((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))) * (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~ (Lower_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~ (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))) * (i3,k))} )
assume A74: 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))) * (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 A75: ( 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 A74, XBOOLE_0:def 4;
hence x in {((Gauge (C,(n + 1))) * (i3,k))} by A10, A59, A67, A70, A75, 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~ (Lower_Seq (C,(n + 1)))) )
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~ (Lower_Seq (C,(n + 1))))
then A76: x = (Gauge (C,(n + 1))) * (i3,k) by TARSKI:def 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 (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;
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 A69, A76, XBOOLE_0:def 4; :: thesis: verum

end;

((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))) * (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~ (Upper_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~ (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))) * (i2,j1))} )
assume A77: 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))) * (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 A78: ( 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 A77, XBOOLE_0:def 4;
hence x in {((Gauge (C,(n + 1))) * (i2,j1))} by A11, A59, A62, A71, A78, 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~ (Upper_Seq (C,(n + 1)))) )
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~ (Upper_Seq (C,(n + 1))))
then A79: x = (Gauge (C,(n + 1))) * (i2,j1) by TARSKI:def 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 (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;
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 A63, A79, XBOOLE_0:def 4; :: thesis: verum

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 Lower_Arc C by A3, A7, A61, A64, A65, A68, A72, A73, Th21, XBOOLE_1:63; :: thesis: verum

end;

suppose 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 Lower_Arc C

then 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~ (Lower_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))} by A1, A4, A7, A8, A10, A14, JORDAN15:12;
A83: 1 < i3 by A1, A80, XXREAL_0:2;
(Gauge (C,(n + 1))) * (i3,k) in (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) by A82, TARSKI:def 1;
then A84: (Gauge (C,(n + 1))) * (i3,k) in L~ (Lower_Seq (C,(n + 1))) by XBOOLE_0:def 4;
A85: 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, A60, A61, JORDAN15:5;
A86: 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, A14, A80, A81, JORDAN15:6;
then A87: (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 A85, XBOOLE_1:13;
A88: ((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))) * (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~ (Lower_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~ (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))) * (i3,k))} )
assume A89: 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))) * (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 A90: ( 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 A89, XBOOLE_0:def 4;
hence x in {((Gauge (C,(n + 1))) * (i3,k))} by A10, A59, A82, A85, A90, 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~ (Lower_Seq (C,(n + 1)))) )
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~ (Lower_Seq (C,(n + 1))))
then A91: x = (Gauge (C,(n + 1))) * (i3,k) by TARSKI:def 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 (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;
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 A84, A91, XBOOLE_0:def 4; :: thesis: verum

end;

((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))) * (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~ (Upper_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~ (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))) * (i2,j1))} )
assume A92: 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))) * (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 A93: ( 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 A92, XBOOLE_0:def 4;
hence x in {((Gauge (C,(n + 1))) * (i2,j1))} by A11, A59, A62, A86, A93, 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~ (Upper_Seq (C,(n + 1)))) )
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~ (Upper_Seq (C,(n + 1))))
then A94: x = (Gauge (C,(n + 1))) * (i2,j1) by TARSKI:def 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 (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;
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 A63, A94, XBOOLE_0:def 4; :: thesis: verum

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 Lower_Arc C by A4, A7, A61, A64, A81, A83, A87, A88, Th23, 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 Lower_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 Lower_Arc C ; :: thesis: verum