let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Lower_Seq (C,n)) holds
ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Lower_Seq (C,n)) holds
ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
let i, j, k be Nat; ( 1 <= j & j <= k & k <= len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Lower_Seq (C,n)) implies ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} ) )
assume that
A1:
1 <= j
and
A2:
j <= k
and
A3:
k <= len (Gauge (C,n))
and
A4:
1 <= i
and
A5:
i <= width (Gauge (C,n))
and
A6:
(Gauge (C,n)) * (j,i) in L~ (Upper_Seq (C,n))
and
A7:
(Gauge (C,n)) * (k,i) in L~ (Lower_Seq (C,n))
; ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
set G = Gauge (C,n);
A8:
len (Gauge (C,n)) = width (Gauge (C,n))
by JORDAN8:def 1;
then A9:
j <= width (Gauge (C,n))
by A2, A3, XXREAL_0:2;
then A10:
[j,i] in Indices (Gauge (C,n))
by A1, A4, A5, A8, MATRIX_0:30;
set s = ((Gauge (C,n)) * (1,i)) `2 ;
set e = (Gauge (C,n)) * (k,i);
set f = (Gauge (C,n)) * (j,i);
set w1 = lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))));
A11:
(Gauge (C,n)) * (k,i) in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))
by RLTOPSP1:68;
then A12:
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets L~ (Lower_Seq (C,n))
by A7, XBOOLE_0:3;
A13:
k >= 1
by A1, A2, XXREAL_0:2;
then
[k,i] in Indices (Gauge (C,n))
by A3, A4, A5, MATRIX_0:30;
then consider k1 being Nat such that
A14:
j <= k1
and
A15:
k1 <= k
and
A16:
((Gauge (C,n)) * (k1,i)) `1 = lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))
by A2, A12, A10, JORDAN1F:3, JORDAN1G:5;
A17:
k1 <= width (Gauge (C,n))
by A3, A8, A15, XXREAL_0:2;
set p = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|;
set w2 = upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))));
set q = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|;
A18:
(Gauge (C,n)) * (j,i) in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))
by RLTOPSP1:68;
then A19:
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i))) meets L~ (Upper_Seq (C,n))
by A6, XBOOLE_0:3;
A20:
1 <= k1
by A1, A14, XXREAL_0:2;
then A21:
((Gauge (C,n)) * (k1,i)) `2 = ((Gauge (C,n)) * (1,i)) `2
by A4, A5, A8, A17, GOBOARD5:1;
then A22:
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| = (Gauge (C,n)) * (k1,i)
by A16, EUCLID:53;
((Gauge (C,n)) * (j,i)) `2 =
((Gauge (C,n)) * (1,i)) `2
by A1, A4, A5, A8, A9, GOBOARD5:1
.=
((Gauge (C,n)) * (k,i)) `2
by A3, A4, A5, A13, GOBOARD5:1
;
then A23:
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) is horizontal
by SPPOL_1:15;
set X = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n)));
reconsider X1 = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) as non empty compact Subset of (TOP-REAL 2) by A6, A18, XBOOLE_0:def 4;
consider pp being object such that
A24:
pp in E-most X1
by XBOOLE_0:def 1;
[k1,i] in Indices (Gauge (C,n))
by A4, A5, A8, A20, A17, MATRIX_0:30;
then consider j1 being Nat such that
A25:
j <= j1
and
A26:
j1 <= k1
and
A27:
((Gauge (C,n)) * (j1,i)) `1 = upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))
by A10, A14, A22, A19, JORDAN1F:4, JORDAN1G:4;
A28:
j1 <= width (Gauge (C,n))
by A17, A26, XXREAL_0:2;
reconsider pp = pp as Point of (TOP-REAL 2) by A24;
A29:
pp in (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n)))
by A24, XBOOLE_0:def 4;
then A30:
pp in L~ (Upper_Seq (C,n))
by XBOOLE_0:def 4;
take
j1
; ex k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
take
k1
; ( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
thus
( j <= j1 & j1 <= k1 & k1 <= k )
by A15, A25, A26; ( (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
A31:
pp in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))
by A29, XBOOLE_0:def 4;
A32:
1 <= j1
by A1, A25, XXREAL_0:2;
then A33:
((Gauge (C,n)) * (j1,i)) `2 = ((Gauge (C,n)) * (1,i)) `2
by A4, A5, A8, A28, GOBOARD5:1;
then A34:
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| = (Gauge (C,n)) * (j1,i)
by A27, EUCLID:53;
then A35:
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 <= |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1
by A4, A5, A8, A17, A22, A26, A32, SPRECT_3:13;
A36: |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 =
E-bound ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))))
by A22, A27, A34, SPRECT_1:46
.=
(E-min ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))))) `1
by EUCLID:52
.=
pp `1
by A24, PSCOMP_1:47
;
A37:
((Gauge (C,n)) * (j,i)) `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2
by A1, A4, A5, A8, A9, A21, A22, GOBOARD5:1;
then
LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|) is horizontal
by SPPOL_1:15;
then
pp `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2
by A21, A22, A33, A34, A31, SPPOL_1:40;
then A38:
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| in L~ (Upper_Seq (C,n))
by A30, A36, TOPREAL3:6;
for x being object holds
( x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n))) iff x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| )
proof
let x be
object ;
( x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n))) iff x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| )
thus
(
x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n))) implies
x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| )
( x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| implies x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n))) )proof
reconsider EE =
(LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n))) as
compact Subset of
(TOP-REAL 2) ;
assume A39:
x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))
;
x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|
then reconsider pp =
x as
Point of
(TOP-REAL 2) ;
A40:
pp in LSeg (
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)
by A39, XBOOLE_0:def 4;
then A41:
pp `1 >= |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1
by A35, TOPREAL1:3;
A42:
((Gauge (C,n)) * (j,i)) `1 <= |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1
by A1, A4, A5, A8, A25, A28, A34, SPRECT_3:13;
reconsider E0 =
proj1 .: EE as
compact Subset of
REAL by Th4;
A43:
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| in LSeg (
((Gauge (C,n)) * (j,i)),
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)
by RLTOPSP1:68;
((Gauge (C,n)) * (j,i)) `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2
by A1, A4, A5, A8, A9, A33, A34, GOBOARD5:1;
then
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| in LSeg (
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,
((Gauge (C,n)) * (j,i)))
by A21, A22, A33, A34, A35, A42, GOBOARD7:8;
then A44:
LSeg (
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)
c= LSeg (
((Gauge (C,n)) * (j,i)),
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)
by A43, TOPREAL1:6;
pp in L~ (Upper_Seq (C,n))
by A39, XBOOLE_0:def 4;
then
pp in EE
by A40, A44, XBOOLE_0:def 4;
then
proj1 . pp in E0
by FUNCT_2:35;
then A45:
pp `1 in E0
by PSCOMP_1:def 5;
E0 is
real-bounded
by RCOMP_1:10;
then
E0 is
bounded_above
by XXREAL_2:def 11;
then
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 >= pp `1
by A27, A34, A45, SEQ_4:def 1;
then A46:
pp `1 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1
by A41, XXREAL_0:1;
pp `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2
by A21, A22, A33, A34, A40, GOBOARD7:6;
hence
x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|
by A46, TOPREAL3:6;
verum
end;
assume A47:
x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|
;
x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))
then
x in LSeg (
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)
by RLTOPSP1:68;
hence
x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))
by A38, A47, XBOOLE_0:def 4;
verum
end;
hence
(LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))}
by A22, A34, TARSKI:def 1; (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))}
set X = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)));
reconsider X1 = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))) as non empty compact Subset of (TOP-REAL 2) by A7, A11, XBOOLE_0:def 4;
consider pp being object such that
A48:
pp in W-most X1
by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A48;
A49:
pp in (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))
by A48, XBOOLE_0:def 4;
then A50:
pp in L~ (Lower_Seq (C,n))
by XBOOLE_0:def 4;
pp in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))
by A49, XBOOLE_0:def 4;
then A51:
pp `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2
by A37, A23, SPPOL_1:40;
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 =
W-bound ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))))
by A16, A22, SPRECT_1:43
.=
(W-min ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))))) `1
by EUCLID:52
.=
pp `1
by A48, PSCOMP_1:31
;
then A52:
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| in L~ (Lower_Seq (C,n))
by A50, A51, TOPREAL3:6;
for x being object holds
( x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n))) iff x = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| )
proof
let x be
object ;
( x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n))) iff x = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| )
thus
(
x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n))) implies
x = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| )
( x = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| implies x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n))) )proof
j1 <= k
by A15, A26, XXREAL_0:2;
then A53:
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 <= ((Gauge (C,n)) * (k,i)) `1
by A3, A4, A5, A32, A34, SPRECT_3:13;
A54:
((Gauge (C,n)) * (k,i)) `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2
by A3, A4, A5, A13, A21, A22, GOBOARD5:1;
A55:
((Gauge (C,n)) * (j,i)) `1 <= |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1
by A1, A4, A5, A8, A14, A17, A22, SPRECT_3:13;
A56:
((Gauge (C,n)) * (j,i)) `1 <= |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1
by A1, A4, A5, A8, A25, A28, A34, SPRECT_3:13;
A57:
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 <= ((Gauge (C,n)) * (k,i)) `1
by A3, A4, A5, A15, A20, A22, SPRECT_3:13;
((Gauge (C,n)) * (j,i)) `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2
by A1, A4, A5, A8, A9, A21, A22, GOBOARD5:1;
then A58:
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| in LSeg (
((Gauge (C,n)) * (j,i)),
((Gauge (C,n)) * (k,i)))
by A54, A55, A57, GOBOARD7:8;
A59:
((Gauge (C,n)) * (k,i)) `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2
by A3, A4, A5, A13, A33, A34, GOBOARD5:1;
((Gauge (C,n)) * (j,i)) `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2
by A1, A4, A5, A8, A9, A33, A34, GOBOARD5:1;
then
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| in LSeg (
((Gauge (C,n)) * (j,i)),
((Gauge (C,n)) * (k,i)))
by A59, A56, A53, GOBOARD7:8;
then A60:
LSeg (
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)
c= LSeg (
((Gauge (C,n)) * (j,i)),
((Gauge (C,n)) * (k,i)))
by A58, TOPREAL1:6;
reconsider EE =
(LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))) as
compact Subset of
(TOP-REAL 2) ;
reconsider E0 =
proj1 .: EE as
compact Subset of
REAL by Th4;
assume A61:
x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n)))
;
x = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|
then reconsider pp =
x as
Point of
(TOP-REAL 2) ;
A62:
pp in LSeg (
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)
by A61, XBOOLE_0:def 4;
then A63:
pp `1 <= |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1
by A35, TOPREAL1:3;
pp in L~ (Lower_Seq (C,n))
by A61, XBOOLE_0:def 4;
then
pp in EE
by A62, A60, XBOOLE_0:def 4;
then
proj1 . pp in E0
by FUNCT_2:35;
then A64:
pp `1 in E0
by PSCOMP_1:def 5;
E0 is
real-bounded
by RCOMP_1:10;
then
E0 is
bounded_below
by XXREAL_2:def 11;
then
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 <= pp `1
by A16, A22, A64, SEQ_4:def 2;
then A65:
pp `1 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1
by A63, XXREAL_0:1;
pp `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2
by A21, A22, A33, A34, A62, GOBOARD7:6;
hence
x = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|
by A65, TOPREAL3:6;
verum
end;
assume A66:
x = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|
;
x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n)))
then
x in LSeg (
|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,
|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)
by RLTOPSP1:68;
hence
x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n)))
by A52, A66, XBOOLE_0:def 4;
verum
end;
hence
(LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))}
by A22, A34, TARSKI:def 1; verum