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

now

per cases ;

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

set X = (LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Upper_Seq C,(n + 1)));
ex x being set 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 set 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 Element of 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:3;
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:57;
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:3;
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: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~ (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:49
.= (S-min ((LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Upper_Seq C,(n + 1))))) `2 by EUCLID:56
.= pp `2 by A21, PSCOMP_1:118 ;
then (Gauge C,(n + 1)) * i2,m in Upper_Arc (L~ (Cage C,(n + 1))) by A18, A30, A23, A31, TOPREAL3:11;
then LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,m) meets Lower_Arc C by A3, A4, A5, A9, A25, A28, Th25;
then LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k) meets Lower_Arc C by A3, A4, A5, A7, A25, A26, Th7, 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:

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:

set X = (LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k)) /\ (L~ (Lower_Seq C,(n + 1)));
ex x being set 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 set 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 Element of 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:2;
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:57;
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:2;
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:63;
|[(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:51
.= (E-min ((LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k)) /\ (L~ (Lower_Seq C,(n + 1))))) `1 by EUCLID:56
.= pp `1 by A33, PSCOMP_1:108 ;
then (Gauge C,(n + 1)) * m,k in Lower_Arc (L~ (Cage C,(n + 1))) by A14, A42, A35, A43, TOPREAL3:11;
then LSeg ((Gauge C,(n + 1)) * m,k),((Gauge C,(n + 1)) * i1,k) meets Lower_Arc C by A2, A7, A8, A10, A38, A40, Th34;
then LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k) meets Lower_Arc C by A2, A3, A7, A10, A37, A38, Th8, 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:

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:

set X = (LSeg ((Gauge C,(n + 1)) * i1,k),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Lower_Seq C,(n + 1)));
ex x being set 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 set 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 Element of 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:2;
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:57;
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:2;
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:63;
|[(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:48
.= (W-min ((LSeg ((Gauge C,(n + 1)) * i1,k),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Lower_Seq C,(n + 1))))) `1 by EUCLID:56
.= pp `1 by A45, PSCOMP_1:88 ;
then (Gauge C,(n + 1)) * m,k in Lower_Arc (L~ (Cage C,(n + 1))) by A14, A54, A47, A55, TOPREAL3:11;
then LSeg ((Gauge C,(n + 1)) * i1,k),((Gauge C,(n + 1)) * m,k) meets Lower_Arc C by A1, A7, A8, A10, A49, A52, Th42;
then LSeg ((Gauge C,(n + 1)) * i1,k),((Gauge C,(n + 1)) * i2,k) meets Lower_Arc C by A1, A4, A7, A10, A49, A50, Th8, 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:

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:

consider j1 being Element of 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, Th11;
(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

per cases ;

suppose A62: i2 <= i1 ; :: thesis:

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, Th7;
consider i3 being Element of 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, Th15;
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, Th8;
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:

proof

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

end;

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

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:

proof

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

end;

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

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 Lower_Arc C by A3, A7, A58, A61, A64, A68, A70, A74, Th47, XBOOLE_1:63; :: thesis:

end;

suppose A78: i1 < i2 ; :: thesis:

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, Th7;
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~ (Upper_Seq C,(n + 1))) = {((Gauge C,(n + 1)) * i3,k)} by A1, A4, A7, A8, A18, A10, A78, Th20;
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, Th8;
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

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

end;

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

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

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

end;

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

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 Lower_Arc C by A4, A7, A58, A61, A81, A84, A86, A90, Th49, 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 Lower_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 Lower_Arc C ; :: thesis: