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