let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

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~ (Lower_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~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} )

let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: 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~ (Lower_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~ (Lower_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~ (Lower_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~ (Lower_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~ (Lower_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~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} )

set G = Gauge (C,n);

A7: k >= 1 by A3, A4, XXREAL_0:2;

then A8: [i,k] in Indices (Gauge (C,n)) by A1, A2, A5, MATRIX_0:30;

set X = (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_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~ (Lower_Seq (C,n))) as non empty compact Subset of (TOP-REAL 2) by A6, XBOOLE_0:def 4;

A10: LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets L~ (Lower_Seq (C,n)) by A6, A9, XBOOLE_0:3;

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~ (Lower_Seq (C,n)))));

A11: j <= width (Gauge (C,n)) by A4, A5, XXREAL_0:2;

then [i,j] in Indices (Gauge (C,n)) by A1, A2, A3, MATRIX_0:30;

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~ (Lower_Seq (C,n))))) by A4, A10, A8, JORDAN1F:2, JORDAN1G:5;

set q = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|;

A15: j1 <= width (Gauge (C,n)) by A5, A13, XXREAL_0:2;

A16: ((Gauge (C,n)) * (i,k)) `1 = ((Gauge (C,n)) * (i,1)) `1 by A1, A2, A5, A7, GOBOARD5:2;

then ((Gauge (C,n)) * (i,j)) `1 = ((Gauge (C,n)) * (i,k)) `1 by A1, A2, A3, A11, GOBOARD5:2;

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~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} )

thus ( j <= j1 & j1 <= k ) by A12, A13; :: thesis: (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_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 (TOP-REAL 2) by A18;

A19: pp in (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) by A18, XBOOLE_0:def 4;

then A20: pp in L~ (Lower_Seq (C,n)) by XBOOLE_0:def 4;

A21: 1 <= j1 by A3, A12, XXREAL_0:2;

then A22: ((Gauge (C,n)) * (i,j1)) `1 = ((Gauge (C,n)) * (i,1)) `1 by A1, A2, A15, GOBOARD5:2;

then A23: |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| = (Gauge (C,n)) * (i,j1) by A14, EUCLID:53;

then A24: |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `2 <= ((Gauge (C,n)) * (i,k)) `2 by A1, A2, A5, A13, A21, SPRECT_3:12;

A25: |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `2 = N-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) by A14, A23, SPRECT_1:45

.= (N-min ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) `2 by EUCLID:52

.= pp `2 by A18, PSCOMP_1:39 ;

pp in LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by A19, XBOOLE_0:def 4;

then pp `1 = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `1 by A16, A22, A23, A17, SPPOL_1:41;

then A26: |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| in L~ (Lower_Seq (C,n)) by A20, A25, TOPREAL3:6;

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~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_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~ (Lower_Seq (C,n))))))]| )

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~ (Lower_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~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} )

let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: 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~ (Lower_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~ (Lower_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~ (Lower_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~ (Lower_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~ (Lower_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~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} )

set G = Gauge (C,n);

A7: k >= 1 by A3, A4, XXREAL_0:2;

then A8: [i,k] in Indices (Gauge (C,n)) by A1, A2, A5, MATRIX_0:30;

set X = (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_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~ (Lower_Seq (C,n))) as non empty compact Subset of (TOP-REAL 2) by A6, XBOOLE_0:def 4;

A10: LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets L~ (Lower_Seq (C,n)) by A6, A9, XBOOLE_0:3;

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~ (Lower_Seq (C,n)))));

A11: j <= width (Gauge (C,n)) by A4, A5, XXREAL_0:2;

then [i,j] in Indices (Gauge (C,n)) by A1, A2, A3, MATRIX_0:30;

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~ (Lower_Seq (C,n))))) by A4, A10, A8, JORDAN1F:2, JORDAN1G:5;

set q = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|;

A15: j1 <= width (Gauge (C,n)) by A5, A13, XXREAL_0:2;

A16: ((Gauge (C,n)) * (i,k)) `1 = ((Gauge (C,n)) * (i,1)) `1 by A1, A2, A5, A7, GOBOARD5:2;

then ((Gauge (C,n)) * (i,j)) `1 = ((Gauge (C,n)) * (i,k)) `1 by A1, A2, A3, A11, GOBOARD5:2;

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~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} )

thus ( j <= j1 & j1 <= k ) by A12, A13; :: thesis: (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_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 (TOP-REAL 2) by A18;

A19: pp in (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) by A18, XBOOLE_0:def 4;

then A20: pp in L~ (Lower_Seq (C,n)) by XBOOLE_0:def 4;

A21: 1 <= j1 by A3, A12, XXREAL_0:2;

then A22: ((Gauge (C,n)) * (i,j1)) `1 = ((Gauge (C,n)) * (i,1)) `1 by A1, A2, A15, GOBOARD5:2;

then A23: |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| = (Gauge (C,n)) * (i,j1) by A14, EUCLID:53;

then A24: |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `2 <= ((Gauge (C,n)) * (i,k)) `2 by A1, A2, A5, A13, A21, SPRECT_3:12;

A25: |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `2 = N-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) by A14, A23, SPRECT_1:45

.= (N-min ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) `2 by EUCLID:52

.= pp `2 by A18, PSCOMP_1:39 ;

pp in LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by A19, XBOOLE_0:def 4;

then pp `1 = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `1 by A16, A22, A23, A17, SPPOL_1:41;

then A26: |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| in L~ (Lower_Seq (C,n)) by A20, A25, TOPREAL3:6;

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~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_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~ (Lower_Seq (C,n))))))]| )

proof

hence
(LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))}
by A23, TARSKI:def 1; :: thesis: verum
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~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_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~ (Lower_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~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_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~ (Lower_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~ (Lower_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~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_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~ (Lower_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~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_Seq (C,n))) by A26, A35, XBOOLE_0:def 4; :: thesis: verum

end;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~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_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~ (Lower_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~ (Lower_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~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_Seq (C,n))) )

proof

assume A35:
x = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_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~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_Seq (C,n)))
reconsider EE = (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))) as compact Subset of (TOP-REAL 2) ;

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~ (Lower_Seq (C,n))))))]| `2 by A1, A2, A3, A12, A15, A23, SPRECT_3:12;

((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~ (Lower_Seq (C,n))))))]| `1 by A1, A2, A3, A11, A22, A23, GOBOARD5:2;

then |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| in LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) by A16, A22, A23, A24, A28, GOBOARD7:7;

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~ (Lower_Seq (C,n))))))]|) c= LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by A27, TOPREAL1:6;

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~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_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~ (Lower_Seq (C,n))))))]|

then reconsider pp = x as Point of (TOP-REAL 2) ;

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~ (Lower_Seq (C,n))))))]|) by A30, XBOOLE_0:def 4;

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~ (Lower_Seq (C,n))))))]| `2 by A24, TOPREAL1:4;

pp in L~ (Lower_Seq (C,n)) by A30, XBOOLE_0:def 4;

then pp in EE by A31, A29, XBOOLE_0:def 4;

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~ (Lower_Seq (C,n))))))]| `2 >= pp `2 by A14, A23, A33, SEQ_4:def 1;

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~ (Lower_Seq (C,n))))))]| `2 by A32, XXREAL_0:1;

pp `1 = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `1 by A16, A22, A23, A31, GOBOARD7:5;

hence x = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| by A34, TOPREAL3:6; :: thesis: verum

end;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~ (Lower_Seq (C,n))))))]| `2 by A1, A2, A3, A12, A15, A23, SPRECT_3:12;

((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~ (Lower_Seq (C,n))))))]| `1 by A1, A2, A3, A11, A22, A23, GOBOARD5:2;

then |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| in LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j))) by A16, A22, A23, A24, A28, GOBOARD7:7;

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~ (Lower_Seq (C,n))))))]|) c= LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by A27, TOPREAL1:6;

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~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_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~ (Lower_Seq (C,n))))))]|

then reconsider pp = x as Point of (TOP-REAL 2) ;

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~ (Lower_Seq (C,n))))))]|) by A30, XBOOLE_0:def 4;

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~ (Lower_Seq (C,n))))))]| `2 by A24, TOPREAL1:4;

pp in L~ (Lower_Seq (C,n)) by A30, XBOOLE_0:def 4;

then pp in EE by A31, A29, XBOOLE_0:def 4;

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~ (Lower_Seq (C,n))))))]| `2 >= pp `2 by A14, A23, A33, SEQ_4:def 1;

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~ (Lower_Seq (C,n))))))]| `2 by A32, XXREAL_0:1;

pp `1 = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `1 by A16, A22, A23, A31, GOBOARD7:5;

hence x = |[(((Gauge (C,n)) * (i,1)) `1),(upper_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| by A34, TOPREAL3:6; :: thesis: verum

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~ (Lower_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~ (Lower_Seq (C,n))))))]|)) /\ (L~ (Lower_Seq (C,n))) by A26, A35, XBOOLE_0:def 4; :: thesis: verum