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)) * (j,i) in L~ (Upper_Seq (C,n)) holds
ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,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)) * (j,i) in L~ (Upper_Seq (C,n)) holds
ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,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)) * (j,i) in L~ (Upper_Seq (C,n)) implies ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,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)) * (j,i) in L~ (Upper_Seq (C,n)) ; :: thesis: ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,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)) * (j,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 w2 = upper_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 j1 being Nat such that
A13: j <= j1 and
A14: j1 <= k and
A15: ((Gauge (C,n)) * (j1,i)) `1 = upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))))) by ;
set q = |[(upper_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: 1 <= j1 by ;
take j1 ; :: thesis: ( j <= j1 & j1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} )
thus ( j <= j1 & j1 <= k ) by ; :: thesis: (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))}
consider pp being object such that
A17: pp in E-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of () by A17;
A18: pp in (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) by ;
then A19: pp in L~ (Upper_Seq (C,n)) by XBOOLE_0:def 4;
A20: j1 <= width (Gauge (C,n)) by ;
then A21: ((Gauge (C,n)) * (j1,i)) `2 = ((Gauge (C,n)) * (1,i)) `2 by ;
then A22: |[(upper_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)) * (j1,i) by ;
then A23: |[(upper_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 ;
A24: ((Gauge (C,n)) * (k,i)) `2 = ((Gauge (C,n)) * (1,i)) `2 by ;
then ((Gauge (C,n)) * (j,i)) `2 = ((Gauge (C,n)) * (k,i)) `2 by ;
then A25: LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) is horizontal by SPPOL_1:15;
A26: |[(upper_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 = E-bound ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)))) by
.= (E-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 = |[(upper_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: |[(upper_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 (((Gauge (C,n)) * (k,i)),|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n))) iff x = |[(upper_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 (((Gauge (C,n)) * (k,i)),|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n))) iff x = |[(upper_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 (((Gauge (C,n)) * (k,i)),|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n))) implies x = |[(upper_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 = |[(upper_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 (((Gauge (C,n)) * (k,i)),|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n))) )
proof
A28: ((Gauge (C,n)) * (j,i)) `1 <= |[(upper_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 ;
((Gauge (C,n)) * (j,i)) `2 = |[(upper_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, A21, A22, GOBOARD5:1;
then A29: |[(upper_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)) * (k,i)),((Gauge (C,n)) * (j,i))) by ;
(Gauge (C,n)) * (k,i) in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by RLTOPSP1:68;
then A30: LSeg (((Gauge (C,n)) * (k,i)),|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|) c= LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by ;
reconsider EE = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) as compact Subset of () ;
reconsider E0 = proj1 .: EE as compact Subset of REAL by Th4;
assume A31: x in (LSeg (((Gauge (C,n)) * (k,i)),|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n))) ; :: thesis: x = |[(upper_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 () ;
A32: pp in LSeg (((Gauge (C,n)) * (k,i)),|[(upper_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 ;
then A33: pp `1 >= |[(upper_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 in L~ (Upper_Seq (C,n)) by ;
then pp in EE by ;
then proj1 . pp in E0 by FUNCT_2:35;
then A34: pp `1 in E0 by PSCOMP_1:def 5;
E0 is real-bounded by RCOMP_1:10;
then E0 is bounded_above by XXREAL_2:def 11;
then |[(upper_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 A35: pp `1 = |[(upper_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 = |[(upper_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 = |[(upper_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 A36: x = |[(upper_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 (((Gauge (C,n)) * (k,i)),|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n)))
then x in LSeg (((Gauge (C,n)) * (k,i)),|[(upper_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 RLTOPSP1:68;
hence x in (LSeg (((Gauge (C,n)) * (k,i)),|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n))) by ; :: thesis: verum
end;
hence (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} by ; :: thesis: verum