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

now

per cases ;

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

then consider m being Element of NAT such that
A19: ( j <= m & m <= k ) and
A20: ((Gauge C,(n + 1)) * i2,m) `2 = inf (proj2 .: ((LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Upper_Seq C,(n + 1))))) by A3, A6, A8, A11, A13, JORDAN1F:1;
A21: ( 1 <= m & m <= width (Gauge C,(n + 1)) ) by A3, A19, XXREAL_0:2;
set X = (LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Upper_Seq C,(n + 1)));
A22: ((Gauge C,(n + 1)) * i2,m) `1 = ((Gauge C,(n + 1)) * i2,1) `1 by A2, A21, GOBOARD5:3;
then A23: |[(((Gauge C,(n + 1)) * i2,1) `1 ),(inf (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 A20, EUCLID:57;
then A24: ((Gauge C,(n + 1)) * i2,j) `1 = |[(((Gauge C,(n + 1)) * i2,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Upper_Seq C,(n + 1))))))]| `1 by A2, A10, A22, 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~ (Upper_Seq C,(n + 1)) ) by A6, A18, 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 PSCOMP_1:64, XBOOLE_0:def 4;
consider pp being set such that
A25: pp in S-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A25;
A26: pp in (LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Upper_Seq C,(n + 1))) by A25, XBOOLE_0:def 4;
then A27: pp in L~ (Upper_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 A26, XBOOLE_0:def 4;
then A28: pp `1 = |[(((Gauge C,(n + 1)) * i2,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Upper_Seq C,(n + 1))))))]| `1 by A14, A24, SPPOL_1:64;
|[(((Gauge C,(n + 1)) * i2,1) `1 ),(inf (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 A20, A23, 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 A25, PSCOMP_1:118 ;
then (Gauge C,(n + 1)) * i2,m in Upper_Arc (L~ (Cage C,(n + 1))) by A6, A23, A27, A28, TOPREAL3:11;
then LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,m) meets Upper_Arc C by A2, A3, A5, A19, A21, Th26;
then LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k) meets Upper_Arc C by A2, A3, A19, 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 Upper_Arc C by XBOOLE_1:70; :: thesis:

end;

suppose A29: ( LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k) meets Lower_Arc (L~ (Cage C,(n + 1))) & i2 <= i1 ) ; :: thesis:

then consider m being Element of NAT such that
A30: ( i2 <= m & m <= i1 ) and
A31: ((Gauge C,(n + 1)) * m,k) `1 = sup (proj1 .: ((LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k)) /\ (L~ (Lower_Seq C,(n + 1))))) by A7, A9, A16, A17, JORDAN1F:4;
A32: ( 1 < m & m < len (Gauge C,(n + 1)) ) by A1, A2, A30, XXREAL_0:2;
set X = (LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k)) /\ (L~ (Lower_Seq C,(n + 1)));
A33: ((Gauge C,(n + 1)) * m,k) `2 = ((Gauge C,(n + 1)) * 1,k) `2 by A12, A32, GOBOARD5:2;
then A34: |[(sup (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 A31, EUCLID:57;
then A35: ((Gauge C,(n + 1)) * i2,k) `2 = |[(sup (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 A2, A12, A33, 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~ (Lower_Seq C,(n + 1)) ) by A7, A29, 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 PSCOMP_1:64, XBOOLE_0:def 4;
consider pp being set such that
A36: pp in E-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A36;
A37: pp in (LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k)) /\ (L~ (Lower_Seq C,(n + 1))) by A36, XBOOLE_0:def 4;
then A38: pp in L~ (Lower_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 A37, XBOOLE_0:def 4;
then A39: pp `2 = |[(sup (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 A15, A35, SPPOL_1:63;
|[(sup (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 A31, A34, 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 A36, PSCOMP_1:108 ;
then (Gauge C,(n + 1)) * m,k in Lower_Arc (L~ (Cage C,(n + 1))) by A7, A34, A38, A39, TOPREAL3:11;
then LSeg ((Gauge C,(n + 1)) * m,k),((Gauge C,(n + 1)) * i1,k) meets Upper_Arc C by A1, A4, A12, A30, A32, Th35;
then LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k) meets Upper_Arc C by A1, A2, A12, A30, 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 Upper_Arc C by XBOOLE_1:70; :: thesis:

end;

suppose A40: ( LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k) meets Lower_Arc (L~ (Cage C,(n + 1))) & i1 < i2 ) ; :: thesis:

then consider m being Element of NAT such that
A41: ( i1 <= m & m <= i2 ) and
A42: ((Gauge C,(n + 1)) * m,k) `1 = inf (proj1 .: ((LSeg ((Gauge C,(n + 1)) * i1,k),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Lower_Seq C,(n + 1))))) by A7, A9, A16, A17, JORDAN1F:3;
A43: ( 1 < m & m < len (Gauge C,(n + 1)) ) by A1, A2, A41, XXREAL_0:2;
set X = (LSeg ((Gauge C,(n + 1)) * i1,k),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Lower_Seq C,(n + 1)));
A44: ((Gauge C,(n + 1)) * m,k) `2 = ((Gauge C,(n + 1)) * 1,k) `2 by A12, A43, GOBOARD5:2;
then A45: |[(inf (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 A42, EUCLID:57;
then A46: ((Gauge C,(n + 1)) * i1,k) `2 = |[(inf (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, A12, A44, 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~ (Lower_Seq C,(n + 1)) ) by A7, A40, 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 PSCOMP_1:64, XBOOLE_0:def 4;
consider pp being set such that
A47: pp in W-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A47;
A48: pp in (LSeg ((Gauge C,(n + 1)) * i1,k),((Gauge C,(n + 1)) * i2,k)) /\ (L~ (Lower_Seq C,(n + 1))) by A47, XBOOLE_0:def 4;
then A49: pp in L~ (Lower_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 A48, XBOOLE_0:def 4;
then A50: pp `2 = |[(inf (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 A15, A46, SPPOL_1:63;
|[(inf (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 A42, A45, 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 A47, PSCOMP_1:88 ;
then (Gauge C,(n + 1)) * m,k in Lower_Arc (L~ (Cage C,(n + 1))) by A7, A45, A49, A50, TOPREAL3:11;
then LSeg ((Gauge C,(n + 1)) * i1,k),((Gauge C,(n + 1)) * m,k) meets Upper_Arc C by A1, A4, A12, A41, A43, Th43;
then LSeg ((Gauge C,(n + 1)) * i1,k),((Gauge C,(n + 1)) * i2,k) meets Upper_Arc C by A1, A2, A12, A41, 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 Upper_Arc C by XBOOLE_1:70; :: thesis:

end;

suppose A51: ( 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
A52: ( j <= j1 & j1 <= k ) and
A53: (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 A2, A3, A5, A7, 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 A53, TARSKI:def 1;
then A54: (Gauge C,(n + 1)) * i2,j1 in L~ (Lower_Seq C,(n + 1)) by XBOOLE_0:def 4;
A55: ( 1 <= j1 & j1 <= width (Gauge C,(n + 1)) ) by A3, A52, XXREAL_0:2;

now

per cases ;

suppose i2 <= i1 ; :: thesis:

then consider i3 being Element of NAT such that
A56: ( i2 <= i3 & i3 <= i1 ) and
A57: (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 A1, A2, A4, A6, A12, Th15;
A58: ( 1 < i3 & i3 < len (Gauge C,(n + 1)) ) by A1, A2, A56, XXREAL_0:2;
(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 A57, TARSKI:def 1;
then A59: (Gauge C,(n + 1)) * i3,k in L~ (Upper_Seq C,(n + 1)) by XBOOLE_0:def 4;
A60: 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 A2, A3, A52, Th7;
A61: 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, A2, A12, A56, Th8;
then A62: (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 A60, XBOOLE_1:13;
A63: ((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 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)) & x in L~ (Upper_Seq C,(n + 1)) ) by XBOOLE_0:def 4;
then ( ( 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) ) & x in L~ (Upper_Seq C,(n + 1)) ) by XBOOLE_0:def 3;
hence x in {((Gauge C,(n + 1)) * i3,k)} by A6, A51, A57, A60, 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 A64: 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~ (Upper_Seq C,(n + 1))) by A59, A64, 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~ (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 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)) & x in L~ (Lower_Seq C,(n + 1)) ) by XBOOLE_0:def 4;
then ( ( 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) ) & x in L~ (Lower_Seq C,(n + 1)) ) by XBOOLE_0:def 3;
hence x in {((Gauge C,(n + 1)) * i2,j1)} by A7, A51, A53, A61, 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 A65: 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~ (Lower_Seq C,(n + 1))) by A54, A65, 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 A2, A3, A52, A55, A56, A58, A62, A63, Th46, XBOOLE_1:63; :: thesis:

end;

suppose i1 < i2 ; :: thesis:

then consider i3 being Element of NAT such that
A66: ( i1 <= i3 & i3 <= i2 ) and
A67: (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, A2, A4, A6, A12, Th20;
A68: ( 1 < i3 & i3 < len (Gauge C,(n + 1)) ) by A1, 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~ (Upper_Seq C,(n + 1))) by A67, 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) c= LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k) by A2, A3, A52, Th7;
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 A1, A2, A12, A66, Th8;
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~ (Upper_Seq C,(n + 1))) = {((Gauge C,(n + 1)) * i3,k)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume 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)) & x in L~ (Upper_Seq C,(n + 1)) ) by XBOOLE_0:def 4;
then ( ( 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) ) & x in L~ (Upper_Seq C,(n + 1)) ) by XBOOLE_0:def 3;
hence x in {((Gauge C,(n + 1)) * i3,k)} by A6, A51, A67, A70, 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 A74: 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~ (Upper_Seq C,(n + 1))) by A69, A74, 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~ (Lower_Seq C,(n + 1))) = {((Gauge C,(n + 1)) * i2,j1)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume 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)) & x in L~ (Lower_Seq C,(n + 1)) ) by XBOOLE_0:def 4;
then ( ( 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) ) & x in L~ (Lower_Seq C,(n + 1)) ) by XBOOLE_0:def 3;
hence x in {((Gauge C,(n + 1)) * i2,j1)} by A7, A51, A53, A71, 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 A75: 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~ (Lower_Seq C,(n + 1))) by A54, A75, 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 A2, A3, A52, A55, A66, A68, A72, A73, Th48, 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: