let n be Nat; :: thesis: for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C

let C be Simple_closed_curve; :: thesis: for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C

let i1, i2, j, k be Nat; :: thesis: ( 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Lower_Arc (L~ (Cage (C,(n + 1)))) implies (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C )
set G = Gauge (C,(n + 1));
assume that
A1: 1 < i1 and
A2: i1 < len (Gauge (C,(n + 1))) and
A3: 1 < i2 and
A4: i2 < len (Gauge (C,(n + 1))) and
A5: 1 <= j and
A6: j <= k and
A7: k <= width (Gauge (C,(n + 1))) and
A8: (Gauge (C,(n + 1))) * (i1,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) and
A9: (Gauge (C,(n + 1))) * (i2,j) in Lower_Arc (L~ (Cage (C,(n + 1)))) ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
A10: 1 <= k by ;
then A11: [i2,k] in Indices (Gauge (C,(n + 1))) by ;
A12: [i1,k] in Indices (Gauge (C,(n + 1))) by ;
((Gauge (C,(n + 1))) * (i2,k)) `2 = ((Gauge (C,(n + 1))) * (1,k)) `2 by
.= ((Gauge (C,(n + 1))) * (i1,k)) `2 by ;
then A13: LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) is horizontal by SPPOL_1:15;
A14: Lower_Arc (L~ (Cage (C,(n + 1)))) = L~ (Lower_Seq (C,(n + 1))) by JORDAN1G:56;
A15: j <= width (Gauge (C,(n + 1))) by ;
then A16: [i2,j] in Indices (Gauge (C,(n + 1))) by ;
((Gauge (C,(n + 1))) * (i2,j)) `1 = ((Gauge (C,(n + 1))) * (i2,1)) `1 by
.= ((Gauge (C,(n + 1))) * (i2,k)) `1 by ;
then A17: LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) is vertical by SPPOL_1:16;
A18: Upper_Arc (L~ (Cage (C,(n + 1)))) = L~ (Upper_Seq (C,(n + 1))) by JORDAN1G:55;
A19: [i2,k] in Indices (Gauge (C,(n + 1))) by ;
now :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
per cases ( LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) meets Upper_Arc (L~ (Cage (C,(n + 1)))) or ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Lower_Arc (L~ (Cage (C,(n + 1)))) & i2 <= i1 ) or ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Lower_Arc (L~ (Cage (C,(n + 1)))) & i1 < i2 ) or ( LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) misses Upper_Arc (L~ (Cage (C,(n + 1)))) & LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) misses Lower_Arc (L~ (Cage (C,(n + 1)))) ) ) ;
suppose A20: LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) meets Upper_Arc (L~ (Cage (C,(n + 1)))) ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
set X = (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))));
ex x being object st
( x in LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) & x in L~ (Upper_Seq (C,(n + 1))) ) by ;
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 () by XBOOLE_0:def 4;
consider pp being object such that
A21: pp in S-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of () 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 ;
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 ;
consider m being Nat such that
A25: j <= m and
A26: m <= k and
A27: ((Gauge (C,(n + 1))) * (i2,m)) `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))) by ;
A28: m <= width (Gauge (C,(n + 1))) by ;
1 <= m by ;
then A29: ((Gauge (C,(n + 1))) * (i2,m)) `1 = ((Gauge (C,(n + 1))) * (i2,1)) `1 by ;
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 ;
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 ;
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 ;
|[(((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
.= (S-min ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))) `2 by EUCLID:52
.= pp `2 by ;
then (Gauge (C,(n + 1))) * (i2,m) in Upper_Arc (L~ (Cage (C,(n + 1)))) by ;
then LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,m))) meets Upper_Arc C by A3, A4, A5, A9, A25, A28, Th24;
then LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) meets Upper_Arc C by A3, A4, A5, A7, A25, A26, Th5, XBOOLE_1:63;
hence (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C by XBOOLE_1:70; :: thesis: verum
end;
suppose A32: ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Lower_Arc (L~ (Cage (C,(n + 1)))) & i2 <= i1 ) ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
set X = (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1))));
ex x being object st
( x in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) & x in L~ (Lower_Seq (C,(n + 1))) ) by ;
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 () by XBOOLE_0:def 4;
consider pp being object such that
A33: pp in E-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of () 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 ;
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 ;
consider m being Nat such that
A37: i2 <= m and
A38: m <= i1 and
A39: ((Gauge (C,(n + 1))) * (m,k)) `1 = upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))) by ;
A40: 1 < m by ;
m < len (Gauge (C,(n + 1))) by ;
then A41: ((Gauge (C,(n + 1))) * (m,k)) `2 = ((Gauge (C,(n + 1))) * (1,k)) `2 by ;
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 ;
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 ;
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 ;
|[(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
.= (E-min ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))) `1 by EUCLID:52
.= pp `1 by ;
then (Gauge (C,(n + 1))) * (m,k) in Lower_Arc (L~ (Cage (C,(n + 1)))) by ;
then LSeg (((Gauge (C,(n + 1))) * (m,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Upper_Arc C by A2, A7, A8, A10, A38, A40, Th33;
then LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Upper_Arc C by ;
hence (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C by XBOOLE_1:70; :: thesis: verum
end;
suppose A44: ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Lower_Arc (L~ (Cage (C,(n + 1)))) & i1 < i2 ) ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
set X = (LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1))));
ex x being object st
( x in LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k))) & x in L~ (Lower_Seq (C,(n + 1))) ) by ;
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 () by XBOOLE_0:def 4;
consider pp being object such that
A45: pp in W-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of () 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 ;
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 ;
consider m being Nat such that
A49: i1 <= m and
A50: m <= i2 and
A51: ((Gauge (C,(n + 1))) * (m,k)) `1 = lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))) by ;
A52: m < len (Gauge (C,(n + 1))) by ;
1 < m by ;
then A53: ((Gauge (C,(n + 1))) * (m,k)) `2 = ((Gauge (C,(n + 1))) * (1,k)) `2 by ;
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 ;
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 ;
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 ;
|[(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
.= (W-min ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))) `1 by EUCLID:52
.= pp `1 by ;
then (Gauge (C,(n + 1))) * (m,k) in Lower_Arc (L~ (Cage (C,(n + 1)))) by ;
then LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (m,k))) meets Upper_Arc C by A1, A7, A8, A10, A49, A52, Th41;
then LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k))) meets Upper_Arc C by ;
hence (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C by XBOOLE_1:70; :: thesis: verum
end;
suppose A56: ( LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) misses Upper_Arc (L~ (Cage (C,(n + 1)))) & LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) misses Lower_Arc (L~ (Cage (C,(n + 1)))) ) ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
consider j1 being Nat such that
A57: j <= j1 and
A58: j1 <= k and
A59: (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i2,j1))} by A3, A4, A5, A6, A7, A9, A14, Th9;
(Gauge (C,(n + 1))) * (i2,j1) in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) by ;
then A60: (Gauge (C,(n + 1))) * (i2,j1) in L~ (Lower_Seq (C,(n + 1))) by XBOOLE_0:def 4;
A61: 1 <= j1 by ;
now :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
per cases ( i2 <= i1 or i1 < i2 ) ;
suppose A62: i2 <= i1 ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
A63: LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) c= LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) by A3, A4, A5, A7, A57, A58, Th5;
consider i3 being Nat such that
A64: i2 <= i3 and
A65: i3 <= i1 and
A66: (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))} by A2, A3, A7, A8, A18, A10, A62, Th13;
A67: LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) c= LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) by A2, A3, A7, A10, A64, A65, Th6;
then A68: (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) c= (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) by ;
(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 ;
then A69: (Gauge (C,(n + 1))) * (i3,k) in L~ (Upper_Seq (C,(n + 1))) by XBOOLE_0:def 4;
A70: ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))}
proof
thus ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) c= {((Gauge (C,(n + 1))) * (i3,k))} :: according to XBOOLE_0:def 10 :: thesis: {((Gauge (C,(n + 1))) * (i3,k))} c= ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) or x in {((Gauge (C,(n + 1))) * (i3,k))} )
assume A71: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) ; :: thesis: x in {((Gauge (C,(n + 1))) * (i3,k))}
then x in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 4;
then A72: ( x in LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) or x in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) ) by XBOOLE_0:def 3;
x in L~ (Upper_Seq (C,(n + 1))) by ;
hence x in {((Gauge (C,(n + 1))) * (i3,k))} by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,(n + 1))) * (i3,k))} or x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) )
(Gauge (C,(n + 1))) * (i3,k) in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) by RLTOPSP1:68;
then A73: (Gauge (C,(n + 1))) * (i3,k) in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 3;
assume x in {((Gauge (C,(n + 1))) * (i3,k))} ; :: thesis: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
then x = (Gauge (C,(n + 1))) * (i3,k) by TARSKI:def 1;
hence x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) by ; :: thesis: verum
end;
A74: ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i2,j1))}
proof
thus ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) c= {((Gauge (C,(n + 1))) * (i2,j1))} :: according to XBOOLE_0:def 10 :: thesis: {((Gauge (C,(n + 1))) * (i2,j1))} c= ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) or x in {((Gauge (C,(n + 1))) * (i2,j1))} )
assume A75: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) ; :: thesis: x in {((Gauge (C,(n + 1))) * (i2,j1))}
then x in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 4;
then A76: ( x in LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) or x in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) ) by XBOOLE_0:def 3;
x in L~ (Lower_Seq (C,(n + 1))) by ;
hence x in {((Gauge (C,(n + 1))) * (i2,j1))} by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,(n + 1))) * (i2,j1))} or x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) )
(Gauge (C,(n + 1))) * (i2,j1) in LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) by RLTOPSP1:68;
then A77: (Gauge (C,(n + 1))) * (i2,j1) in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 3;
assume x in {((Gauge (C,(n + 1))) * (i2,j1))} ; :: thesis: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
then x = (Gauge (C,(n + 1))) * (i2,j1) by TARSKI:def 1;
hence x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) by ; :: thesis: verum
end;
i3 < len (Gauge (C,(n + 1))) by ;
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 ; :: thesis: verum
end;
suppose A78: i1 < i2 ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
A79: LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) c= LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) by A3, A4, A5, A7, A57, A58, Th5;
consider i3 being Nat such that
A80: i1 <= i3 and
A81: i3 <= i2 and
A82: (LSeg (((Gauge (C,(n + 1))) * (i3,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))} by A1, A4, A7, A8, A18, A10, A78, Th18;
A83: LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) c= LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) by A1, A4, A7, A10, A80, A81, Th6;
then A84: (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) c= (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) by ;
(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 ;
then A85: (Gauge (C,(n + 1))) * (i3,k) in L~ (Upper_Seq (C,(n + 1))) by XBOOLE_0:def 4;
A86: ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))}
proof
thus ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) c= {((Gauge (C,(n + 1))) * (i3,k))} :: according to XBOOLE_0:def 10 :: thesis: {((Gauge (C,(n + 1))) * (i3,k))} c= ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) or x in {((Gauge (C,(n + 1))) * (i3,k))} )
assume A87: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) ; :: thesis: x in {((Gauge (C,(n + 1))) * (i3,k))}
then x in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 4;
then A88: ( x in LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) or x in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) ) by XBOOLE_0:def 3;
x in L~ (Upper_Seq (C,(n + 1))) by ;
hence x in {((Gauge (C,(n + 1))) * (i3,k))} by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,(n + 1))) * (i3,k))} or x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) )
(Gauge (C,(n + 1))) * (i3,k) in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) by RLTOPSP1:68;
then A89: (Gauge (C,(n + 1))) * (i3,k) in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 3;
assume x in {((Gauge (C,(n + 1))) * (i3,k))} ; :: thesis: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
then x = (Gauge (C,(n + 1))) * (i3,k) by TARSKI:def 1;
hence x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) by ; :: thesis: verum
end;
A90: ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i2,j1))}
proof
thus ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) c= {((Gauge (C,(n + 1))) * (i2,j1))} :: according to XBOOLE_0:def 10 :: thesis: {((Gauge (C,(n + 1))) * (i2,j1))} c= ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) or x in {((Gauge (C,(n + 1))) * (i2,j1))} )
assume A91: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) ; :: thesis: x in {((Gauge (C,(n + 1))) * (i2,j1))}
then x in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 4;
then A92: ( x in LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) or x in LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))) ) by XBOOLE_0:def 3;
x in L~ (Lower_Seq (C,(n + 1))) by ;
hence x in {((Gauge (C,(n + 1))) * (i2,j1))} by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((Gauge (C,(n + 1))) * (i2,j1))} or x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) )
(Gauge (C,(n + 1))) * (i2,j1) in LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k))) by RLTOPSP1:68;
then A93: (Gauge (C,(n + 1))) * (i2,j1) in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) by XBOOLE_0:def 3;
assume x in {((Gauge (C,(n + 1))) * (i2,j1))} ; :: thesis: x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
then x = (Gauge (C,(n + 1))) * (i2,j1) by TARSKI:def 1;
hence x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) by ; :: thesis: verum
end;
1 < i3 by ;
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 ; :: thesis: verum
end;
end;
end;
hence (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C ; :: thesis: verum
end;
end;
end;
hence (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C ; :: thesis: verum