let n be Element of NAT ; :: thesis:
let C be Simple_closed_curve; :: thesis:
let i1, i2, j, k be Element of NAT ; :: thesis:
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:
A10: Lower_Arc (L~ (Cage C,(n + 1))) = L~ (Lower_Seq C,(n + 1)) by JORDAN1G:64;
A11: Upper_Arc (L~ (Cage C,(n + 1))) = L~ (Upper_Seq C,(n + 1)) by JORDAN1G:63;
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_1:37;
A14: 1 <= k by A5, A6, XXREAL_0:2;
then A15: [i2,k] in Indices (Gauge C,(n + 1)) by A3, A4, A7, MATRIX_1:37;
((Gauge C,(n + 1)) * i2,j) `1 = ((Gauge C,(n + 1)) * i2,1) `1 by A3, A4, A5, A12, GOBOARD5:3
.= ((Gauge C,(n + 1)) * i2,k) `1 by A3, A4, A7, A14, GOBOARD5:3 ;
then A16: LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k) is vertical by SPPOL_1:37;
((Gauge C,(n + 1)) * i2,k) `2 = ((Gauge C,(n + 1)) * 1,k) `2 by A3, A4, A7, A14, GOBOARD5:2
.= ((Gauge C,(n + 1)) * i1,k) `2 by A1, A2, A7, A14, GOBOARD5:2 ;
then A17: LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k) is horizontal by SPPOL_1:36;
A18: [i2,k] in Indices (Gauge C,(n + 1)) by A3, A4, A7, A14, MATRIX_1:37;
A19: [i1,k] in Indices (Gauge C,(n + 1)) by A1, A2, A7, A14, MATRIX_1:37;

now

per cases ;

suppose A20: LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k) meets Lower_Arc (L~ (Cage C,(n + 1))) ; :: thesis:

then consider m being Element of 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)));
A26: ((Gauge C,(n + 1)) * i2,m) `1 = ((Gauge C,(n + 1)) * i2,1) `1 by A3, A4, A24, A25, GOBOARD5:3;
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:57;
then 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, A26, GOBOARD5:3;
ex x being set 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 set 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:64;
|[(((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 A23, A27, SPRECT_1:49
.= (S-min ((LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Lower_Seq C,(n + 1))))) `2 by EUCLID:56
.= pp `2 by A29, PSCOMP_1:118 ;
then (Gauge C,(n + 1)) * i2,m in Lower_Arc (L~ (Cage C,(n + 1))) by A10, A27, A31, A32, TOPREAL3:11;
then LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,m) meets Upper_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 Upper_Arc C by A3, A4, A5, A7, A21, A22, JORDAN15:7, 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:

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:

then consider m being Element of 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)));
A39: ((Gauge C,(n + 1)) * m,k) `2 = ((Gauge C,(n + 1)) * 1,k) `2 by A7, A14, A37, A38, GOBOARD5:2;
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:57;
then 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, A39, GOBOARD5:2;
ex x being set 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 set 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:63;
|[(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 A36, A40, SPRECT_1:51
.= (E-min ((LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k)) /\ (L~ (Upper_Seq C,(n + 1))))) `1 by EUCLID:56
.= pp `1 by A42, PSCOMP_1:108 ;
then (Gauge C,(n + 1)) * m,k in Upper_Arc (L~ (Cage C,(n + 1))) by A11, A40, A44, A45, TOPREAL3:11;
then LSeg ((Gauge C,(n + 1)) * m,k),((Gauge C,(n + 1)) * i1,k) meets Upper_Arc C by A2, A7, A8, A14, A35, A37, JORDAN15:43;
then LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k) meets Upper_Arc C by A2, A3, A7, A14, A34, A35, JORDAN15:8, 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:

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:

then consider m being Element of 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)));
A52: ((Gauge C,(n + 1)) * m,k) `2 = ((Gauge C,(n + 1)) * 1,k) `2 by A7, A14, A50, A51, GOBOARD5:2;
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:57;
then 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, A52, GOBOARD5:2;
ex x being set 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 set 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:63;
|[(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 A49, A53, SPRECT_1:48
.= (W-min ((LSeg ((Gauge C,(n + 1)) * i1,k),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Upper_Seq C,(n + 1))))) `1 by EUCLID:56
.= pp `1 by A55, PSCOMP_1:88 ;
then (Gauge C,(n + 1)) * m,k in Upper_Arc (L~ (Cage C,(n + 1))) by A11, A53, A57, A58, TOPREAL3:11;
then LSeg ((Gauge C,(n + 1)) * i1,k),((Gauge C,(n + 1)) * m,k) meets Upper_Arc C by A1, A7, A8, A14, A47, A51, JORDAN15:35;
then LSeg ((Gauge C,(n + 1)) * i1,k),((Gauge C,(n + 1)) * i2,k) meets Upper_Arc C by A1, A4, A7, A14, A47, A48, JORDAN15:8, 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:

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:

consider j1 being Element of 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:17;
(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

per cases ;

suppose i2 <= i1 ; :: thesis:

then consider i3 being Element of 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:21;
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:7;
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:8;
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:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
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:
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:3, XBOOLE_0:def 4; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {((Gauge C,(n + 1)) * i3,k)} ; :: thesis:
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:69;
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:

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:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
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:
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:3, XBOOLE_0:def 4; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {((Gauge C,(n + 1)) * i2,j1)} ; :: thesis:
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:69;
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:

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

end;

suppose i1 < i2 ; :: thesis:

then consider i3 being Element of 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:14;
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:7;
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:8;
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

let x be set ; :: according to TARSKI:def 3 :: thesis:
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:
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:3, XBOOLE_0:def 4; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {((Gauge C,(n + 1)) * i3,k)} ; :: thesis:
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:69;
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:

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

let x be set ; :: according to TARSKI:def 3 :: thesis:
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:
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:3, XBOOLE_0:def 4; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {((Gauge C,(n + 1)) * i2,j1)} ; :: thesis:
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:69;
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:

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 by A4, A7, A61, A64, A81, A83, A87, A88, Th23, XBOOLE_1:63; :: thesis:

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:

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: