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