let n be Nat; for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Lower_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Upper_Arc (L~ (Cage (C,(n + 1)))) holds
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
let C be Simple_closed_curve; for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Lower_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Upper_Arc (L~ (Cage (C,(n + 1)))) holds
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
let i1, i2, j, k be Nat; ( 1 < i1 & i1 < len (Gauge (C,(n + 1))) & 1 < i2 & i2 < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i1,k) in Lower_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * (i2,j) in Upper_Arc (L~ (Cage (C,(n + 1)))) implies (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets 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 Lower_Arc (L~ (Cage (C,(n + 1))))
and
A9:
(Gauge (C,(n + 1))) * (i2,j) in Upper_Arc (L~ (Cage (C,(n + 1))))
; (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:
Lower_Arc (L~ (Cage (C,(n + 1)))) = L~ (Lower_Seq (C,(n + 1)))
by JORDAN1G:56;
A11:
Upper_Arc (L~ (Cage (C,(n + 1)))) = L~ (Upper_Seq (C,(n + 1)))
by JORDAN1G:55;
A12:
j <= width (Gauge (C,(n + 1)))
by A6, A7, XXREAL_0:2;
then A13:
[i2,j] in Indices (Gauge (C,(n + 1)))
by A3, A4, A5, MATRIX_0:30;
A14:
1 <= k
by A5, A6, XXREAL_0:2;
then A15:
[i2,k] in Indices (Gauge (C,(n + 1)))
by A3, A4, A7, MATRIX_0:30;
((Gauge (C,(n + 1))) * (i2,j)) `1 =
((Gauge (C,(n + 1))) * (i2,1)) `1
by A3, A4, A5, A12, GOBOARD5:2
.=
((Gauge (C,(n + 1))) * (i2,k)) `1
by A3, A4, A7, A14, GOBOARD5:2
;
then A16:
LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) is vertical
by SPPOL_1:16;
((Gauge (C,(n + 1))) * (i2,k)) `2 =
((Gauge (C,(n + 1))) * (1,k)) `2
by A3, A4, A7, A14, GOBOARD5:1
.=
((Gauge (C,(n + 1))) * (i1,k)) `2
by A1, A2, A7, A14, GOBOARD5:1
;
then A17:
LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) is horizontal
by SPPOL_1:15;
A18:
[i2,k] in Indices (Gauge (C,(n + 1)))
by A3, A4, A7, A14, MATRIX_0:30;
A19:
[i1,k] in Indices (Gauge (C,(n + 1)))
by A1, A2, A7, A14, MATRIX_0:30;
now (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 Cper cases
( LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) meets Lower_Arc (L~ (Cage (C,(n + 1)))) or ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Upper_Arc (L~ (Cage (C,(n + 1)))) & i2 <= i1 ) or ( LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) meets Upper_Arc (L~ (Cage (C,(n + 1)))) & i1 < i2 ) or ( LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k))) misses Lower_Arc (L~ (Cage (C,(n + 1)))) & LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))) misses Upper_Arc (L~ (Cage (C,(n + 1)))) ) )
;
suppose A20:
LSeg (
((Gauge (C,(n + 1))) * (i2,j)),
((Gauge (C,(n + 1))) * (i2,k)))
meets Lower_Arc (L~ (Cage (C,(n + 1))))
;
(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 Cthen consider m being
Nat such that A21:
j <= m
and A22:
m <= k
and A23:
((Gauge (C,(n + 1))) * (i2,m)) `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))))
by A6, A10, A13, A15, JORDAN1F:1, JORDAN1G:5;
A24:
1
<= m
by A5, A21, XXREAL_0:2;
A25:
m <= width (Gauge (C,(n + 1)))
by A7, A22, XXREAL_0:2;
set X =
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1))));
A26:
((Gauge (C,(n + 1))) * (i2,m)) `1 = ((Gauge (C,(n + 1))) * (i2,1)) `1
by A3, A4, A24, A25, GOBOARD5:2;
then A27:
|[(((Gauge (C,(n + 1))) * (i2,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))))]| = (Gauge (C,(n + 1))) * (
i2,
m)
by A23, EUCLID:53;
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:2;
ex
x being
object st
(
x in LSeg (
((Gauge (C,(n + 1))) * (i2,j)),
((Gauge (C,(n + 1))) * (i2,k))) &
x in L~ (Lower_Seq (C,(n + 1))) )
by A10, A20, XBOOLE_0:3;
then reconsider X1 =
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) as non
empty compact Subset of
(TOP-REAL 2) by XBOOLE_0:def 4;
consider pp being
object such that A29:
pp in S-most X1
by XBOOLE_0:def 1;
reconsider pp =
pp as
Point of
(TOP-REAL 2) by A29;
A30:
pp in (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))
by A29, XBOOLE_0:def 4;
then A31:
pp in L~ (Lower_Seq (C,(n + 1)))
by XBOOLE_0:def 4;
pp in LSeg (
((Gauge (C,(n + 1))) * (i2,j)),
((Gauge (C,(n + 1))) * (i2,k)))
by A30, XBOOLE_0:def 4;
then A32:
pp `1 = |[(((Gauge (C,(n + 1))) * (i2,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))))]| `1
by A16, A28, SPPOL_1:41;
|[(((Gauge (C,(n + 1))) * (i2,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))))]| `2 =
S-bound ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))
by A23, A27, SPRECT_1:44
.=
(S-min ((LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))))) `2
by EUCLID:52
.=
pp `2
by A29, PSCOMP_1:55
;
then
(Gauge (C,(n + 1))) * (
i2,
m)
in Lower_Arc (L~ (Cage (C,(n + 1))))
by A10, A27, A31, A32, TOPREAL3:6;
then
LSeg (
((Gauge (C,(n + 1))) * (i2,j)),
((Gauge (C,(n + 1))) * (i2,m)))
meets Upper_Arc C
by A3, A4, A5, A9, A21, A25, Th18;
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:5, XBOOLE_1:63;
hence
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
by XBOOLE_1:70;
verum end; suppose A33:
(
LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i1,k)))
meets Upper_Arc (L~ (Cage (C,(n + 1)))) &
i2 <= i1 )
;
(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 Cthen consider m being
Nat such that A34:
i2 <= m
and A35:
m <= i1
and A36:
((Gauge (C,(n + 1))) * (m,k)) `1 = upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))
by A11, A18, A19, JORDAN1F:4, JORDAN1G:4;
A37:
1
< m
by A3, A34, XXREAL_0:2;
A38:
m < len (Gauge (C,(n + 1)))
by A2, A35, XXREAL_0:2;
set X =
(LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1))));
A39:
((Gauge (C,(n + 1))) * (m,k)) `2 = ((Gauge (C,(n + 1))) * (1,k)) `2
by A7, A14, A37, A38, GOBOARD5:1;
then A40:
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| = (Gauge (C,(n + 1))) * (
m,
k)
by A36, EUCLID:53;
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:1;
ex
x being
object st
(
x in LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i1,k))) &
x in L~ (Upper_Seq (C,(n + 1))) )
by A11, A33, XBOOLE_0:3;
then reconsider X1 =
(LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) as non
empty compact Subset of
(TOP-REAL 2) by XBOOLE_0:def 4;
consider pp being
object such that A42:
pp in E-most X1
by XBOOLE_0:def 1;
reconsider pp =
pp as
Point of
(TOP-REAL 2) by A42;
A43:
pp in (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))
by A42, XBOOLE_0:def 4;
then A44:
pp in L~ (Upper_Seq (C,(n + 1)))
by XBOOLE_0:def 4;
pp in LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i1,k)))
by A43, XBOOLE_0:def 4;
then A45:
pp `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `2
by A17, A41, SPPOL_1:40;
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `1 =
E-bound ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))
by A36, A40, SPRECT_1:46
.=
(E-min ((LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))) `1
by EUCLID:52
.=
pp `1
by A42, PSCOMP_1:47
;
then
(Gauge (C,(n + 1))) * (
m,
k)
in Upper_Arc (L~ (Cage (C,(n + 1))))
by A11, A40, A44, A45, TOPREAL3:6;
then
LSeg (
((Gauge (C,(n + 1))) * (m,k)),
((Gauge (C,(n + 1))) * (i1,k)))
meets Upper_Arc C
by A2, A7, A8, A14, A35, A37, JORDAN15:41;
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:6, XBOOLE_1:63;
hence
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
by XBOOLE_1:70;
verum end; suppose A46:
(
LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i1,k)))
meets Upper_Arc (L~ (Cage (C,(n + 1)))) &
i1 < i2 )
;
(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 Cthen consider m being
Nat such that A47:
i1 <= m
and A48:
m <= i2
and A49:
((Gauge (C,(n + 1))) * (m,k)) `1 = lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))
by A11, A18, A19, JORDAN1F:3, JORDAN1G:4;
A50:
1
< m
by A1, A47, XXREAL_0:2;
A51:
m < len (Gauge (C,(n + 1)))
by A4, A48, XXREAL_0:2;
set X =
(LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))));
A52:
((Gauge (C,(n + 1))) * (m,k)) `2 = ((Gauge (C,(n + 1))) * (1,k)) `2
by A7, A14, A50, A51, GOBOARD5:1;
then A53:
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| = (Gauge (C,(n + 1))) * (
m,
k)
by A49, EUCLID:53;
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:1;
ex
x being
object st
(
x in LSeg (
((Gauge (C,(n + 1))) * (i1,k)),
((Gauge (C,(n + 1))) * (i2,k))) &
x in L~ (Upper_Seq (C,(n + 1))) )
by A11, A46, XBOOLE_0:3;
then reconsider X1 =
(LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) as non
empty compact Subset of
(TOP-REAL 2) by XBOOLE_0:def 4;
consider pp being
object such that A55:
pp in W-most X1
by XBOOLE_0:def 1;
reconsider pp =
pp as
Point of
(TOP-REAL 2) by A55;
A56:
pp in (LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))
by A55, XBOOLE_0:def 4;
then A57:
pp in L~ (Upper_Seq (C,(n + 1)))
by XBOOLE_0:def 4;
pp in LSeg (
((Gauge (C,(n + 1))) * (i1,k)),
((Gauge (C,(n + 1))) * (i2,k)))
by A56, XBOOLE_0:def 4;
then A58:
pp `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `2
by A17, A54, SPPOL_1:40;
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))))),(((Gauge (C,(n + 1))) * (1,k)) `2)]| `1 =
W-bound ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))
by A49, A53, SPRECT_1:43
.=
(W-min ((LSeg (((Gauge (C,(n + 1))) * (i1,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))))) `1
by EUCLID:52
.=
pp `1
by A55, PSCOMP_1:31
;
then
(Gauge (C,(n + 1))) * (
m,
k)
in Upper_Arc (L~ (Cage (C,(n + 1))))
by A11, A53, A57, A58, TOPREAL3:6;
then
LSeg (
((Gauge (C,(n + 1))) * (i1,k)),
((Gauge (C,(n + 1))) * (m,k)))
meets Upper_Arc C
by A1, A7, A8, A14, A47, A51, JORDAN15:33;
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:6, XBOOLE_1:63;
hence
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
by XBOOLE_1:70;
verum end; suppose A59:
(
LSeg (
((Gauge (C,(n + 1))) * (i2,j)),
((Gauge (C,(n + 1))) * (i2,k)))
misses Lower_Arc (L~ (Cage (C,(n + 1)))) &
LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i1,k)))
misses Upper_Arc (L~ (Cage (C,(n + 1)))) )
;
(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 Cconsider j1 being
Nat such that A60:
j <= j1
and A61:
j1 <= k
and A62:
(LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i2,j1))}
by A3, A4, A5, A6, A7, A9, A11, JORDAN15:15;
(Gauge (C,(n + 1))) * (
i2,
j1)
in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Upper_Seq (C,(n + 1))))
by A62, TARSKI:def 1;
then A63:
(Gauge (C,(n + 1))) * (
i2,
j1)
in L~ (Upper_Seq (C,(n + 1)))
by XBOOLE_0:def 4;
A64:
1
<= j1
by A5, A60, XXREAL_0:2;
now (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 Cper cases
( i2 <= i1 or i1 < i2 )
;
suppose
i2 <= i1
;
(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 Cthen consider i3 being
Nat such that A65:
i2 <= i3
and A66:
i3 <= i1
and A67:
(LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))}
by A2, A3, A7, A8, A10, A14, JORDAN15:19;
A68:
i3 < len (Gauge (C,(n + 1)))
by A2, A66, XXREAL_0:2;
(Gauge (C,(n + 1))) * (
i3,
k)
in (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))
by A67, TARSKI:def 1;
then A69:
(Gauge (C,(n + 1))) * (
i3,
k)
in L~ (Lower_Seq (C,(n + 1)))
by XBOOLE_0:def 4;
A70:
LSeg (
((Gauge (C,(n + 1))) * (i2,j1)),
((Gauge (C,(n + 1))) * (i2,k)))
c= LSeg (
((Gauge (C,(n + 1))) * (i2,j)),
((Gauge (C,(n + 1))) * (i2,k)))
by A3, A4, A5, A7, A60, A61, JORDAN15:5;
A71:
LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i3,k)))
c= LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i1,k)))
by A2, A3, A7, A14, A65, A66, JORDAN15:6;
then A72:
(LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) c= (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))))
by A70, XBOOLE_1:13;
A73:
((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))}
proof
thus
((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) c= {((Gauge (C,(n + 1))) * (i3,k))}
XBOOLE_0:def 10 {((Gauge (C,(n + 1))) * (i3,k))} c= ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))proof
let x be
object ;
TARSKI:def 3 ( not x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) or x in {((Gauge (C,(n + 1))) * (i3,k))} )
assume A74:
x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
;
x in {((Gauge (C,(n + 1))) * (i3,k))}
then
x in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))
by XBOOLE_0:def 4;
then A75:
(
x in LSeg (
((Gauge (C,(n + 1))) * (i2,j1)),
((Gauge (C,(n + 1))) * (i2,k))) or
x in LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i3,k))) )
by XBOOLE_0:def 3;
x in L~ (Lower_Seq (C,(n + 1)))
by A74, XBOOLE_0:def 4;
hence
x in {((Gauge (C,(n + 1))) * (i3,k))}
by A10, A59, A67, A70, A75, XBOOLE_0:def 4;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in {((Gauge (C,(n + 1))) * (i3,k))} or x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) )
assume
x in {((Gauge (C,(n + 1))) * (i3,k))}
;
x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
then A76:
x = (Gauge (C,(n + 1))) * (
i3,
k)
by TARSKI:def 1;
(Gauge (C,(n + 1))) * (
i3,
k)
in LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i3,k)))
by RLTOPSP1:68;
then
(Gauge (C,(n + 1))) * (
i3,
k)
in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))
by XBOOLE_0:def 3;
hence
x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
by A69, A76, XBOOLE_0:def 4;
verum
end;
((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i2,j1))}
proof
thus
((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) c= {((Gauge (C,(n + 1))) * (i2,j1))}
XBOOLE_0:def 10 {((Gauge (C,(n + 1))) * (i2,j1))} c= ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))proof
let x be
object ;
TARSKI:def 3 ( not x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) or x in {((Gauge (C,(n + 1))) * (i2,j1))} )
assume A77:
x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
;
x in {((Gauge (C,(n + 1))) * (i2,j1))}
then
x in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))
by XBOOLE_0:def 4;
then A78:
(
x in LSeg (
((Gauge (C,(n + 1))) * (i2,j1)),
((Gauge (C,(n + 1))) * (i2,k))) or
x in LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i3,k))) )
by XBOOLE_0:def 3;
x in L~ (Upper_Seq (C,(n + 1)))
by A77, XBOOLE_0:def 4;
hence
x in {((Gauge (C,(n + 1))) * (i2,j1))}
by A11, A59, A62, A71, A78, XBOOLE_0:def 4;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in {((Gauge (C,(n + 1))) * (i2,j1))} or x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) )
assume
x in {((Gauge (C,(n + 1))) * (i2,j1))}
;
x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
then A79:
x = (Gauge (C,(n + 1))) * (
i2,
j1)
by TARSKI:def 1;
(Gauge (C,(n + 1))) * (
i2,
j1)
in LSeg (
((Gauge (C,(n + 1))) * (i2,j1)),
((Gauge (C,(n + 1))) * (i2,k)))
by RLTOPSP1:68;
then
(Gauge (C,(n + 1))) * (
i2,
j1)
in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))
by XBOOLE_0:def 3;
hence
x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
by A63, A79, XBOOLE_0:def 4;
verum
end; hence
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
by A3, A7, A61, A64, A65, A68, A72, A73, Th20, XBOOLE_1:63;
verum end; suppose
i1 < i2
;
(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 Cthen consider i3 being
Nat such that A80:
i1 <= i3
and A81:
i3 <= i2
and A82:
(LSeg (((Gauge (C,(n + 1))) * (i3,k)),((Gauge (C,(n + 1))) * (i2,k)))) /\ (L~ (Lower_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))}
by A1, A4, A7, A8, A10, A14, JORDAN15:12;
A83:
1
< i3
by A1, A80, XXREAL_0:2;
(Gauge (C,(n + 1))) * (
i3,
k)
in (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) /\ (L~ (Lower_Seq (C,(n + 1))))
by A82, TARSKI:def 1;
then A84:
(Gauge (C,(n + 1))) * (
i3,
k)
in L~ (Lower_Seq (C,(n + 1)))
by XBOOLE_0:def 4;
A85:
LSeg (
((Gauge (C,(n + 1))) * (i2,j1)),
((Gauge (C,(n + 1))) * (i2,k)))
c= LSeg (
((Gauge (C,(n + 1))) * (i2,j)),
((Gauge (C,(n + 1))) * (i2,k)))
by A3, A4, A5, A7, A60, A61, JORDAN15:5;
A86:
LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i3,k)))
c= LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i1,k)))
by A1, A4, A7, A14, A80, A81, JORDAN15:6;
then A87:
(LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k)))) c= (LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k))))
by A85, XBOOLE_1:13;
A88:
((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i3,k))}
proof
thus
((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) c= {((Gauge (C,(n + 1))) * (i3,k))}
XBOOLE_0:def 10 {((Gauge (C,(n + 1))) * (i3,k))} c= ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))proof
let x be
object ;
TARSKI:def 3 ( not x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) or x in {((Gauge (C,(n + 1))) * (i3,k))} )
assume A89:
x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
;
x in {((Gauge (C,(n + 1))) * (i3,k))}
then
x in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))
by XBOOLE_0:def 4;
then A90:
(
x in LSeg (
((Gauge (C,(n + 1))) * (i2,j1)),
((Gauge (C,(n + 1))) * (i2,k))) or
x in LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i3,k))) )
by XBOOLE_0:def 3;
x in L~ (Lower_Seq (C,(n + 1)))
by A89, XBOOLE_0:def 4;
hence
x in {((Gauge (C,(n + 1))) * (i3,k))}
by A10, A59, A82, A85, A90, XBOOLE_0:def 4;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in {((Gauge (C,(n + 1))) * (i3,k))} or x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1)))) )
assume
x in {((Gauge (C,(n + 1))) * (i3,k))}
;
x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
then A91:
x = (Gauge (C,(n + 1))) * (
i3,
k)
by TARSKI:def 1;
(Gauge (C,(n + 1))) * (
i3,
k)
in LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i3,k)))
by RLTOPSP1:68;
then
(Gauge (C,(n + 1))) * (
i3,
k)
in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))
by XBOOLE_0:def 3;
hence
x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Lower_Seq (C,(n + 1))))
by A84, A91, XBOOLE_0:def 4;
verum
end;
((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) = {((Gauge (C,(n + 1))) * (i2,j1))}
proof
thus
((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) c= {((Gauge (C,(n + 1))) * (i2,j1))}
XBOOLE_0:def 10 {((Gauge (C,(n + 1))) * (i2,j1))} c= ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))proof
let x be
object ;
TARSKI:def 3 ( not x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) or x in {((Gauge (C,(n + 1))) * (i2,j1))} )
assume A92:
x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
;
x in {((Gauge (C,(n + 1))) * (i2,j1))}
then
x in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))
by XBOOLE_0:def 4;
then A93:
(
x in LSeg (
((Gauge (C,(n + 1))) * (i2,j1)),
((Gauge (C,(n + 1))) * (i2,k))) or
x in LSeg (
((Gauge (C,(n + 1))) * (i2,k)),
((Gauge (C,(n + 1))) * (i3,k))) )
by XBOOLE_0:def 3;
x in L~ (Upper_Seq (C,(n + 1)))
by A92, XBOOLE_0:def 4;
hence
x in {((Gauge (C,(n + 1))) * (i2,j1))}
by A11, A59, A62, A86, A93, XBOOLE_0:def 4;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in {((Gauge (C,(n + 1))) * (i2,j1))} or x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1)))) )
assume
x in {((Gauge (C,(n + 1))) * (i2,j1))}
;
x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
then A94:
x = (Gauge (C,(n + 1))) * (
i2,
j1)
by TARSKI:def 1;
(Gauge (C,(n + 1))) * (
i2,
j1)
in LSeg (
((Gauge (C,(n + 1))) * (i2,j1)),
((Gauge (C,(n + 1))) * (i2,k)))
by RLTOPSP1:68;
then
(Gauge (C,(n + 1))) * (
i2,
j1)
in (LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))
by XBOOLE_0:def 3;
hence
x in ((LSeg (((Gauge (C,(n + 1))) * (i2,j1)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i3,k))))) /\ (L~ (Upper_Seq (C,(n + 1))))
by A63, A94, XBOOLE_0:def 4;
verum
end; hence
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C
by A4, A7, A61, A64, A81, A83, A87, A88, Th22, XBOOLE_1:63;
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
;
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
; verum