let n be Element of NAT ; :: thesis: 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) & (Gauge C,n) * i,k in L~ (Upper_Seq C,n) holds
ex j1, k1 being Element of 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); :: thesis: 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) & (Gauge C,n) * i,k in L~ (Upper_Seq C,n) holds
ex j1, k1 being Element of 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 Element of NAT ; :: thesis: ( 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 Element of 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 & i <= len (Gauge C,n) )
and
A2:
( 1 <= j & j <= k & k <= width (Gauge C,n) )
and
A3:
(Gauge C,n) * i,j in L~ (Lower_Seq C,n)
and
A4:
(Gauge C,n) * i,k in L~ (Upper_Seq C,n)
; :: thesis: ex j1, k1 being Element of 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;
set s = ((Gauge C,n) * i,1) `1 ;
set f = (Gauge C,n) * i,j;
set e = (Gauge C,n) * i,k;
set w1 = inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n))));
set p = |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|;
set w2 = sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)))))]|;
A5:
Upper_Seq C,n is_sequence_on Gauge C,n
by JORDAN1G:4;
A6:
(Gauge C,n) * i,k in LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)
by RLTOPSP1:69;
then A7:
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets L~ (Upper_Seq C,n)
by A4, XBOOLE_0:3;
A8:
j <= width (Gauge C,n)
by A2, XXREAL_0:2;
then A9:
[i,j] in Indices (Gauge C,n)
by A1, A2, MATRIX_1:37;
A10:
k >= 1
by A2, XXREAL_0:2;
then
[i,k] in Indices (Gauge C,n)
by A1, A2, MATRIX_1:37;
then consider k1 being Element of NAT such that
A11:
( j <= k1 & k1 <= k )
and
A12:
((Gauge C,n) * i,k1) `2 = inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n))))
by A2, A5, A7, A9, JORDAN1F:1;
A13:
( 1 <= k1 & k1 <= width (Gauge C,n) )
by A2, A11, XXREAL_0:2;
then A14:
((Gauge C,n) * i,k1) `1 = ((Gauge C,n) * i,1) `1
by A1, GOBOARD5:3;
then A15:
|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| = (Gauge C,n) * i,k1
by A12, EUCLID:57;
A16:
Lower_Seq C,n is_sequence_on Gauge C,n
by JORDAN1G:5;
A17:
(Gauge C,n) * i,j in LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k1)
by RLTOPSP1:69;
then A18:
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k1) meets L~ (Lower_Seq C,n)
by A3, XBOOLE_0:3;
[i,k1] in Indices (Gauge C,n)
by A1, A13, MATRIX_1:37;
then consider j1 being Element of NAT such that
A19:
( j <= j1 & j1 <= k1 )
and
A20:
((Gauge C,n) * i,j1) `2 = sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n))))
by A9, A11, A15, A16, A18, JORDAN1F:2;
A21:
( 1 <= j1 & j1 <= width (Gauge C,n) )
by A2, A13, A19, XXREAL_0:2;
then A22:
((Gauge C,n) * i,j1) `1 = ((Gauge C,n) * i,1) `1
by A1, GOBOARD5:3;
then A23:
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 A20, EUCLID:57;
take
j1
; :: thesis: ex k1 being Element of 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
; :: thesis: ( 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 A11, A19; :: thesis: ( (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)} )
A24:
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| `2
by A1, A13, A15, A19, A21, A23, SPRECT_3:24;
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 A3, A17, PSCOMP_1:64, XBOOLE_0:def 4;
consider pp being set such that
A25:
pp in N-most X1
by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A25;
A26:
pp in (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k1)) /\ (L~ (Lower_Seq C,n))
by A25, XBOOLE_0:def 4;
then A27:
pp in L~ (Lower_Seq C,n)
by XBOOLE_0:def 4;
A28:
pp in LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k1)
by A26, XBOOLE_0:def 4;
A29:
((Gauge C,n) * i,j) `1 = |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| `1
by A1, A2, A8, A14, A15, GOBOARD5:3;
then
LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| is vertical
by SPPOL_1:37;
then A30:
pp `1 = |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)))))]| `1
by A14, A15, A22, A23, A28, SPPOL_1:64;
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 A15, A20, A23, SPRECT_1:50
.=
(N-min ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k1)) /\ (L~ (Lower_Seq C,n)))) `2
by EUCLID:56
.=
pp `2
by A25, PSCOMP_1:98
;
then A31:
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 A27, A30, TOPREAL3:11;
for x being set holds
( x in (LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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
set ;
:: thesis: ( x in (LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)))))]| )
:: thesis: ( x = |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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
assume A32:
x in (LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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))
;
:: thesis: x = |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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) ;
A33:
pp in LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)))))]|
by A32, XBOOLE_0:def 4;
then A34:
pp `1 = |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)))))]| `1
by A14, A15, A22, A23, GOBOARD7:5;
A35:
pp `2 >= |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)))))]| `2
by A24, A33, TOPREAL1:10;
reconsider EE =
(LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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) by PSCOMP_1:64;
reconsider E0 =
proj2 .: EE as
compact Subset of
REAL by JCT_MISC:24;
A36:
((Gauge C,n) * i,j) `1 = |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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, A8, A22, A23, GOBOARD5:3;
((Gauge C,n) * i,j) `2 <= |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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, A19, A21, A23, SPRECT_3:24;
then A37:
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,
((Gauge C,n) * i,j)
by A14, A15, A22, A23, A24, A36, GOBOARD7:8;
|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|
by RLTOPSP1:69;
then A38:
LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|
by A37, TOPREAL1:12;
E0 is
bounded
by RCOMP_1:28;
then A39:
E0 is
bounded_above
by XXREAL_2:def 11;
pp in L~ (Lower_Seq C,n)
by A32, XBOOLE_0:def 4;
then
pp in EE
by A33, A38, XBOOLE_0:def 4;
then
proj2 . pp in E0
by FUNCT_2:43;
then
pp `2 in E0
by PSCOMP_1:def 29;
then
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 A20, A23, A39, SEQ_4:def 4;
then
pp `2 = |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)))))]| `2
by A35, XXREAL_0:1;
hence
x = |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)))))]|
by A34, TOPREAL3:11;
:: thesis: verum
end;
assume A40:
x = |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)))))]|
;
:: thesis: x in (LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)))))]|
by RLTOPSP1:69;
hence
x in (LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 A31, A40, XBOOLE_0:def 4;
:: thesis: 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 A15, A23, TARSKI:def 1; :: thesis: (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 A4, A6, PSCOMP_1:64, XBOOLE_0:def 4;
consider pp being set such that
A41:
pp in S-most X1
by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A41;
A42:
pp in (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n))
by A41, XBOOLE_0:def 4;
then A43:
pp in L~ (Upper_Seq C,n)
by XBOOLE_0:def 4;
A44:
pp in LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)
by A42, XBOOLE_0:def 4;
((Gauge C,n) * i,j) `1 =
((Gauge C,n) * i,1) `1
by A1, A2, A8, GOBOARD5:3
.=
((Gauge C,n) * i,k) `1
by A1, A2, A10, GOBOARD5:3
;
then
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) is vertical
by SPPOL_1:37;
then A45:
pp `1 = |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| `1
by A29, A44, SPPOL_1:64;
|[(((Gauge C,n) * i,1) `1 ),(inf (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 A12, A15, SPRECT_1:49
.=
(S-min ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))) `2
by EUCLID:56
.=
pp `2
by A41, PSCOMP_1:118
;
then A46:
|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| in L~ (Upper_Seq C,n)
by A43, A45, TOPREAL3:11;
for x being set holds
( x in (LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| )
proof
let x be
set ;
:: thesis: ( x in (LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(inf (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 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| )
:: thesis: ( x = |[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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
assume A47:
x in (LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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))
;
:: thesis: x = |[(((Gauge C,n) * i,1) `1 ),(inf (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) ;
A48:
pp in LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)))))]|
by A47, XBOOLE_0:def 4;
then A49:
pp `1 = |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| `1
by A14, A15, A22, A23, GOBOARD7:5;
A50:
pp `2 <= |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| `2
by A24, A48, TOPREAL1:10;
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) by PSCOMP_1:64;
reconsider E0 =
proj2 .: EE as
compact Subset of
REAL by JCT_MISC:24;
A51:
((Gauge C,n) * i,j) `1 = |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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, A8, A22, A23, GOBOARD5:3;
A52:
((Gauge C,n) * i,k) `1 = |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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, A10, A22, A23, GOBOARD5:3;
A53:
((Gauge C,n) * i,j) `2 <= |[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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, A19, A21, A23, SPRECT_3:24;
j1 <= k
by A11, A19, XXREAL_0:2;
then
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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, A21, A23, SPRECT_3:24;
then A54:
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 A51, A52, A53, GOBOARD7:8;
A55:
((Gauge C,n) * i,j) `1 = |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| `1
by A1, A2, A8, A14, A15, GOBOARD5:3;
A56:
((Gauge C,n) * i,k) `1 = |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| `1
by A1, A2, A10, A14, A15, GOBOARD5:3;
A57:
((Gauge C,n) * i,j) `2 <= |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| `2
by A1, A2, A11, A13, A15, SPRECT_3:24;
|[(((Gauge C,n) * i,1) `1 ),(inf (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, A11, A13, A15, SPRECT_3:24;
then
|[(((Gauge C,n) * i,1) `1 ),(inf (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 A55, A56, A57, GOBOARD7:8;
then A58:
LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 A54, TOPREAL1:12;
E0 is
bounded
by RCOMP_1:28;
then A59:
E0 is
bounded_below
by XXREAL_2:def 11;
pp in L~ (Upper_Seq C,n)
by A47, XBOOLE_0:def 4;
then
pp in EE
by A48, A58, XBOOLE_0:def 4;
then
proj2 . pp in E0
by FUNCT_2:43;
then
pp `2 in E0
by PSCOMP_1:def 29;
then
|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| `2 <= pp `2
by A12, A15, A59, SEQ_4:def 5;
then
pp `2 = |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]| `2
by A50, XXREAL_0:1;
hence
x = |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|
by A49, TOPREAL3:11;
:: thesis: verum
end;
assume A60:
x = |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|
;
:: thesis: x in (LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,
|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|) /\ (L~ (Lower_Seq C,n)))))]|
by RLTOPSP1:69;
hence
x in (LSeg |[(((Gauge C,n) * i,1) `1 ),(inf (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)))))]|,|[(((Gauge C,n) * i,1) `1 ),(sup (proj2 .: ((LSeg ((Gauge C,n) * i,j),|[(((Gauge C,n) * i,1) `1 ),(inf (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 A46, A60, XBOOLE_0:def 4;
:: thesis: 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 A15, A23, TARSKI:def 1; :: thesis: verum