let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of ()
for i, j, k being 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~ (Upper_Seq (C,n)) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j,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 (); :: thesis: for i, j, k being 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~ (Upper_Seq (C,n)) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )

let i, j, k be Nat; :: thesis: ( 1 <= j & j <= k & k <= len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) implies ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_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~ (Upper_Seq (C,n)) ; :: thesis: ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )

set G = Gauge (C,n);
A7: k >= 1 by ;
then A8: [k,i] in Indices (Gauge (C,n)) by ;
set X = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)));
A9: (Gauge (C,n)) * (k,i) in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by RLTOPSP1:68;
then reconsider X1 = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) as non empty compact Subset of () by ;
A10: LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets L~ (Upper_Seq (C,n)) by ;
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~ (Upper_Seq (C,n)))));
A11: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then A12: j <= width (Gauge (C,n)) by ;
then [j,i] in Indices (Gauge (C,n)) by ;
then consider k1 being 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~ (Upper_Seq (C,n))))) by ;
set p = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|;
A16: k1 <= width (Gauge (C,n)) by ;
((Gauge (C,n)) * (j,i)) `2 = ((Gauge (C,n)) * (1,i)) `2 by
.= ((Gauge (C,n)) * (k,i)) `2 by ;
then A17: LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) is horizontal by SPPOL_1:15;
take k1 ; :: thesis: ( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
thus ( j <= k1 & k1 <= k ) by ; :: thesis: (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))}
consider pp being object such that
A18: pp in W-most X1 by XBOOLE_0:def 1;
A19: 1 <= k1 by ;
then A20: ((Gauge (C,n)) * (k1,i)) `2 = ((Gauge (C,n)) * (1,i)) `2 by ;
then A21: |[(lower_bound (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 ;
then A22: ((Gauge (C,n)) * (j,i)) `1 <= |[(lower_bound (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 ;
A23: ((Gauge (C,n)) * (j,i)) `2 = |[(lower_bound (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, A4, A5, A11, A12, A20, A21, GOBOARD5:1;
reconsider pp = pp as Point of () by A18;
A24: pp in (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) by ;
then A25: pp in L~ (Upper_Seq (C,n)) by XBOOLE_0:def 4;
A26: |[(lower_bound (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
.= (W-min ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))))) `1 by EUCLID:52
.= pp `1 by ;
pp in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by ;
then pp `2 = |[(lower_bound (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 ;
then A27: |[(lower_bound (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 ;
for x being object holds
( x in (LSeg (|[(lower_bound (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)))) /\ (L~ (Upper_Seq (C,n))) iff x = |[(lower_bound (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 object ; :: thesis: ( x in (LSeg (|[(lower_bound (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)))) /\ (L~ (Upper_Seq (C,n))) iff x = |[(lower_bound (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 (|[(lower_bound (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)))) /\ (L~ (Upper_Seq (C,n))) implies x = |[(lower_bound (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 = |[(lower_bound (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 (|[(lower_bound (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)))) /\ (L~ (Upper_Seq (C,n))) )
proof
reconsider EE = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) as compact Subset of () ;
assume A28: x in (LSeg (|[(lower_bound (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)))) /\ (L~ (Upper_Seq (C,n))) ; :: thesis: x = |[(lower_bound (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 () ;
A29: pp in LSeg (|[(lower_bound (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 ;
then A30: pp `1 <= |[(lower_bound (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 ;
A31: |[(lower_bound (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 ;
A32: ((Gauge (C,n)) * (j,i)) `1 <= |[(lower_bound (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 ;
A33: ((Gauge (C,n)) * (k,i)) `2 = |[(lower_bound (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 A3, A4, A5, A7, A20, A21, GOBOARD5:1;
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:68;
((Gauge (C,n)) * (j,i)) `2 = |[(lower_bound (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, A4, A5, A11, A12, A20, A21, GOBOARD5:1;
then |[(lower_bound (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 ;
then A35: LSeg (|[(lower_bound (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))) c= LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by ;
pp in L~ (Upper_Seq (C,n)) by ;
then pp in EE by ;
then proj1 . pp in E0 by FUNCT_2:35;
then A36: pp `1 in E0 by PSCOMP_1:def 5;
E0 is real-bounded by RCOMP_1:10;
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~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 <= pp `1 by ;
then A37: pp `1 = |[(lower_bound (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 ;
pp `2 = |[(lower_bound (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 ;
hence x = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| by ; :: thesis: verum
end;
assume A38: x = |[(lower_bound (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 (|[(lower_bound (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)))) /\ (L~ (Upper_Seq (C,n)))
then x in LSeg (|[(lower_bound (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 RLTOPSP1:68;
hence x in (LSeg (|[(lower_bound (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)))) /\ (L~ (Upper_Seq (C,n))) by ; :: thesis: verum
end;
hence (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} by ; :: thesis: verum