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

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

let i, j, k be 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~ (Upper_Seq (C,n)) implies ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} ) )

assume that
A1: 1 <= i and
A2: i <= len (Gauge (C,n)) and
A3: 1 <= j and
A4: j <= k and
A5: k <= width (Gauge (C,n)) and
A6: (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) ; :: thesis: ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} )

set G = Gauge (C,n);
A7: k >= 1 by ;
then A8: [i,k] in Indices (Gauge (C,n)) by ;
set X = (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)));
A9: (Gauge (C,n)) * (i,j) in LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by RLTOPSP1:68;
then reconsider X1 = (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) as non empty compact Subset of () by ;
A10: LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets L~ (Upper_Seq (C,n)) by ;
set s = ((Gauge (C,n)) * (i,1)) `1 ;
set e = (Gauge (C,n)) * (i,k);
set f = (Gauge (C,n)) * (i,j);
set w2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))));
A11: j <= width (Gauge (C,n)) by ;
then [i,j] in Indices (Gauge (C,n)) by ;
then consider j1 being Nat such that
A12: j <= j1 and
A13: j1 <= k and
A14: ((Gauge (C,n)) * (i,j1)) `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) by ;
set q = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|;
A15: j1 <= width (Gauge (C,n)) by ;
A16: ((Gauge (C,n)) * (i,k)) `1 = ((Gauge (C,n)) * (i,1)) `1 by ;
then ((Gauge (C,n)) * (i,j)) `1 = ((Gauge (C,n)) * (i,k)) `1 by ;
then A17: LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) is vertical by SPPOL_1:16;
take j1 ; :: thesis: ( j <= j1 & j1 <= k & (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} )
thus ( j <= j1 & j1 <= k ) by ; :: thesis: (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))}
consider pp being object such that
A18: pp in N-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of () by A18;
A19: pp in (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) by ;
then A20: pp in L~ (Upper_Seq (C,n)) by XBOOLE_0:def 4;
A21: 1 <= j1 by ;
then A22: ((Gauge (C,n)) * (i,j1)) `1 = ((Gauge (C,n)) * (i,1)) `1 by ;
then A23: |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| = (Gauge (C,n)) * (i,j1) by ;
then A24: |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (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 ;
A25: |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| `2 = N-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) by
.= (N-min ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))) `2 by EUCLID:52
.= pp `2 by ;
pp in LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by ;
then pp `1 = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| `1 by ;
then A26: |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| in L~ (Upper_Seq (C,n)) by ;
for x being object holds
( x in (LSeg (((Gauge (C,n)) * (i,k)),|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|)) /\ (L~ (Upper_Seq (C,n))) iff x = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| )
proof
let x be object ; :: thesis: ( x in (LSeg (((Gauge (C,n)) * (i,k)),|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|)) /\ (L~ (Upper_Seq (C,n))) iff x = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (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,k)),|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|)) /\ (L~ (Upper_Seq (C,n))) implies x = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (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),(upper_bound (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,k)),|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|)) /\ (L~ (Upper_Seq (C,n))) )
proof
reconsider EE = (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) as compact Subset of () ;
reconsider E0 = proj2 .: EE as compact Subset of REAL by JCT_MISC:15;
A27: (Gauge (C,n)) * (i,k) in LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by RLTOPSP1:68;
A28: ((Gauge (C,n)) * (i,j)) `2 <= |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| `2 by ;
((Gauge (C,n)) * (i,j)) `1 = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| `1 by ;
then |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| in LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) by ;
then A29: LSeg (((Gauge (C,n)) * (i,k)),|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|) c= LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by ;
assume A30: x in (LSeg (((Gauge (C,n)) * (i,k)),|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|)) /\ (L~ (Upper_Seq (C,n))) ; :: thesis: x = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|
then reconsider pp = x as Point of () ;
A31: pp in LSeg (((Gauge (C,n)) * (i,k)),|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|) by ;
then A32: pp `2 >= |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| `2 by ;
pp in L~ (Upper_Seq (C,n)) by ;
then pp in EE by ;
then proj2 . pp in E0 by FUNCT_2:35;
then A33: pp `2 in E0 by PSCOMP_1:def 6;
E0 is real-bounded by RCOMP_1:10;
then E0 is bounded_above by XXREAL_2:def 11;
then |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| `2 >= pp `2 by ;
then A34: pp `2 = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| `2 by ;
pp `1 = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| `1 by ;
hence x = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| by ; :: thesis: verum
end;
assume A35: x = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (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,k)),|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|)) /\ (L~ (Upper_Seq (C,n)))
then x in LSeg (((Gauge (C,n)) * (i,k)),|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|) by RLTOPSP1:68;
hence x in (LSeg (((Gauge (C,n)) * (i,k)),|[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]|)) /\ (L~ (Upper_Seq (C,n))) by ; :: thesis: verum
end;
hence (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} by ; :: thesis: verum