let n be Element of NAT ; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Element of 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) holds
ex j1 being Element of NAT st
( j <= j1 & j1 <= k & (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j1)} )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for i, j, k being Element of 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) holds
ex j1 being Element of NAT st
( j <= j1 & j1 <= k & (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j1)} )
let i, j, k be Element of 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) implies ex j1 being Element of NAT st
( j <= j1 & j1 <= k & (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j1)} ) )
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)
; ex j1 being Element of NAT st
( j <= j1 & j1 <= k & (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j1)} )
set G = Gauge C,n;
A7:
k >= 1
by A3, A4, XXREAL_0:2;
then A8:
[i,k] in Indices (Gauge C,n)
by A1, A2, A5, MATRIX_1:37;
set X = (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n));
A9:
(Gauge C,n) * i,j in LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)
by RLTOPSP1:69;
then reconsider X1 = (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) as non empty compact Subset of (TOP-REAL 2) by A6, XBOOLE_0:def 4;
A10:
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets L~ (Lower_Seq C,n)
by A6, A9, XBOOLE_0:3;
set s = ((Gauge C,n) * i,1) `1 ;
set e = (Gauge C,n) * i,k;
set f = (Gauge C,n) * i,j;
set w2 = upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n))));
A11:
j <= width (Gauge C,n)
by A4, A5, XXREAL_0:2;
then
[i,j] in Indices (Gauge C,n)
by A1, A2, A3, MATRIX_1:37;
then consider j1 being Element of NAT such that
A12:
j <= j1
and
A13:
j1 <= k
and
A14:
((Gauge C,n) * i,j1) `2 = upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n))))
by A4, A10, A8, JORDAN1F:2, JORDAN1G:5;
set q = |[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]|;
A15:
j1 <= width (Gauge C,n)
by A5, A13, XXREAL_0:2;
A16:
((Gauge C,n) * i,k) `1 = ((Gauge C,n) * i,1) `1
by A1, A2, A5, A7, GOBOARD5:3;
then
((Gauge C,n) * i,j) `1 = ((Gauge C,n) * i,k) `1
by A1, A2, A3, A11, GOBOARD5:3;
then A17:
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) is vertical
by SPPOL_1:37;
take
j1
; ( j <= j1 & j1 <= k & (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j1)} )
thus
( j <= j1 & j1 <= k )
by A12, A13; (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j1)}
consider pp being set such that
A18:
pp in N-most X1
by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A18;
A19:
pp in (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n))
by A18, XBOOLE_0:def 4;
then A20:
pp in L~ (Lower_Seq C,n)
by XBOOLE_0:def 4;
A21:
1 <= j1
by A3, A12, XXREAL_0:2;
then A22:
((Gauge C,n) * i,j1) `1 = ((Gauge C,n) * i,1) `1
by A1, A2, A15, GOBOARD5:3;
then A23:
|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]| = (Gauge C,n) * i,j1
by A14, EUCLID:57;
then A24:
|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]| `2 <= ((Gauge C,n) * i,k) `2
by A1, A2, A5, A13, A21, SPRECT_3:24;
A25: |[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]| `2 =
N-bound ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))
by A14, A23, SPRECT_1:50
.=
(N-min ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))) `2
by EUCLID:56
.=
pp `2
by A18, PSCOMP_1:98
;
pp in LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)
by A19, XBOOLE_0:def 4;
then
pp `1 = |[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]| `1
by A16, A22, A23, A17, SPPOL_1:64;
then A26:
|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]| in L~ (Lower_Seq C,n)
by A20, A25, TOPREAL3:11;
for x being set holds
( x in (LSeg ((Gauge C,n) * i,k),|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (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,k)) /\ (L~ (Lower_Seq C,n)))))]| )
proof
let x be
set ;
( x in (LSeg ((Gauge C,n) * i,k),|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (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,k)) /\ (L~ (Lower_Seq C,n)))))]| )
thus
(
x in (LSeg ((Gauge C,n) * i,k),|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (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,k)) /\ (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,k)) /\ (L~ (Lower_Seq C,n)))))]| implies x in (LSeg ((Gauge C,n) * i,k),|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)) )proof
reconsider EE =
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) as
compact Subset of
(TOP-REAL 2) ;
reconsider E0 =
proj2 .: EE as
compact Subset of
REAL by JCT_MISC:24;
A27:
(Gauge C,n) * i,
k in LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k)
by RLTOPSP1:69;
A28:
((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,k)) /\ (L~ (Lower_Seq C,n)))))]| `2
by A1, A2, A3, A12, A15, A23, SPRECT_3:24;
((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,k)) /\ (L~ (Lower_Seq C,n)))))]| `1
by A1, A2, A3, A11, A22, A23, GOBOARD5:3;
then
|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]| in LSeg ((Gauge C,n) * i,k),
((Gauge C,n) * i,j)
by A16, A22, A23, A24, A28, GOBOARD7:8;
then A29:
LSeg ((Gauge C,n) * i,k),
|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]| c= LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k)
by A27, TOPREAL1:12;
assume A30:
x in (LSeg ((Gauge C,n) * i,k),|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (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,k)) /\ (L~ (Lower_Seq C,n)))))]|
then reconsider pp =
x as
Point of
(TOP-REAL 2) ;
A31:
pp in LSeg ((Gauge C,n) * i,k),
|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]|
by A30, XBOOLE_0:def 4;
then A32:
pp `2 >= |[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]| `2
by A24, TOPREAL1:10;
pp in L~ (Lower_Seq C,n)
by A30, XBOOLE_0:def 4;
then
pp in EE
by A31, A29, XBOOLE_0:def 4;
then
proj2 . pp in E0
by FUNCT_2:43;
then A33:
pp `2 in E0
by PSCOMP_1:def 29;
E0 is
bounded
by RCOMP_1:28;
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,k)) /\ (L~ (Lower_Seq C,n)))))]| `2 >= pp `2
by A14, A23, A33, SEQ_4:def 4;
then A34:
pp `2 = |[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]| `2
by A32, XXREAL_0:1;
pp `1 = |[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]| `1
by A16, A22, A23, A31, GOBOARD7:5;
hence
x = |[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]|
by A34, TOPREAL3:11;
verum
end;
assume A35:
x = |[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]|
;
x in (LSeg ((Gauge C,n) * i,k),|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n))
then
x in LSeg ((Gauge C,n) * i,k),
|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]|
by RLTOPSP1:69;
hence
x in (LSeg ((Gauge C,n) * i,k),|[(((Gauge C,n) * i,1) `1 ),(upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n))
by A26, A35, XBOOLE_0:def 4;
verum
end;
hence
(LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j1)}
by A23, TARSKI:def 1; verum