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