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,k) in L~ (Lower_Seq (C,n)) holds

ex k1 being Nat st

( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )

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,k) in L~ (Lower_Seq (C,n)) holds

ex k1 being Nat st

( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )

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,k) in L~ (Lower_Seq (C,n)) implies ex k1 being Nat st

( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} ) )

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,k) in L~ (Lower_Seq (C,n)) ; :: thesis: ex k1 being Nat st

( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )

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,k) 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 w1 = lower_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 k1 being Nat such that

A12: j <= k1 and

A13: k1 <= k and

A14: ((Gauge (C,n)) * (i,k1)) `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) by A4, A10, A8, JORDAN1F:1, JORDAN1G:5;

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

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

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

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

then A16: LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) is vertical by SPPOL_1:16;

take k1 ; :: thesis: ( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )

thus ( j <= k1 & k1 <= k ) by A12, A13; :: thesis: (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))}

consider pp being object such that

A17: pp in S-most X1 by XBOOLE_0:def 1;

A18: 1 <= k1 by A3, A12, XXREAL_0:2;

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

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

then A21: ((Gauge (C,n)) * (i,j)) `2 <= |[(((Gauge (C,n)) * (i,1)) `1),(lower_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, SPRECT_3:12;

A22: ((Gauge (C,n)) * (i,j)) `1 = |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `1 by A1, A2, A3, A11, A19, A20, GOBOARD5:2;

reconsider pp = pp as Point of (TOP-REAL 2) by A17;

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

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

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

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

.= pp `2 by A17, PSCOMP_1:55 ;

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

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

then A26: |[(((Gauge (C,n)) * (i,1)) `1),(lower_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 A24, A25, TOPREAL3:6;

for x being object holds

( x in (LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) iff x = |[(((Gauge (C,n)) * (i,1)) `1),(lower_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,k) in L~ (Lower_Seq (C,n)) holds

ex k1 being Nat st

( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )

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,k) in L~ (Lower_Seq (C,n)) holds

ex k1 being Nat st

( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )

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,k) in L~ (Lower_Seq (C,n)) implies ex k1 being Nat st

( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} ) )

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,k) in L~ (Lower_Seq (C,n)) ; :: thesis: ex k1 being Nat st

( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )

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,k) 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 w1 = lower_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 k1 being Nat such that

A12: j <= k1 and

A13: k1 <= k and

A14: ((Gauge (C,n)) * (i,k1)) `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))) by A4, A10, A8, JORDAN1F:1, JORDAN1G:5;

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

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

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

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

then A16: LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) is vertical by SPPOL_1:16;

take k1 ; :: thesis: ( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )

thus ( j <= k1 & k1 <= k ) by A12, A13; :: thesis: (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))}

consider pp being object such that

A17: pp in S-most X1 by XBOOLE_0:def 1;

A18: 1 <= k1 by A3, A12, XXREAL_0:2;

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

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

then A21: ((Gauge (C,n)) * (i,j)) `2 <= |[(((Gauge (C,n)) * (i,1)) `1),(lower_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, SPRECT_3:12;

A22: ((Gauge (C,n)) * (i,j)) `1 = |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `1 by A1, A2, A3, A11, A19, A20, GOBOARD5:2;

reconsider pp = pp as Point of (TOP-REAL 2) by A17;

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

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

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

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

.= pp `2 by A17, PSCOMP_1:55 ;

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

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

then A26: |[(((Gauge (C,n)) * (i,1)) `1),(lower_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 A24, A25, TOPREAL3:6;

for x being object holds

( x in (LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) iff x = |[(((Gauge (C,n)) * (i,1)) `1),(lower_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,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))}
by A20, TARSKI:def 1; :: thesis: verum
let x be object ; :: thesis: ( x in (LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) iff x = |[(((Gauge (C,n)) * (i,1)) `1),(lower_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,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) implies x = |[(((Gauge (C,n)) * (i,1)) `1),(lower_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),(lower_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,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) )

then x in LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j))) by RLTOPSP1:68;

hence x in (LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) by A26, A37, XBOOLE_0:def 4; :: thesis: verum

end;thus ( x in (LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) implies x = |[(((Gauge (C,n)) * (i,1)) `1),(lower_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),(lower_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,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) )

proof

assume A37:
x = |[(((Gauge (C,n)) * (i,1)) `1),(lower_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,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (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,j) in LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by RLTOPSP1:68;

A28: ((Gauge (C,n)) * (i,k)) `1 = |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `1 by A1, A2, A5, A7, A19, A20, GOBOARD5:2;

A29: |[(((Gauge (C,n)) * (i,1)) `1),(lower_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, A18, A20, SPRECT_3:12;

A30: ((Gauge (C,n)) * (i,j)) `2 <= |[(((Gauge (C,n)) * (i,1)) `1),(lower_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, A20, SPRECT_3:12;

((Gauge (C,n)) * (i,j)) `1 = |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `1 by A1, A2, A3, A11, A19, A20, GOBOARD5:2;

then |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| in LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by A28, A30, A29, GOBOARD7:7;

then A31: LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j))) c= LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by A27, TOPREAL1:6;

assume A32: x in (LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) ; :: thesis: x = |[(((Gauge (C,n)) * (i,1)) `1),(lower_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) ;

A33: pp in LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j))) by A32, XBOOLE_0:def 4;

then A34: pp `2 <= |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `2 by A21, TOPREAL1:4;

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

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

then proj2 . pp in E0 by FUNCT_2:35;

then A35: pp `2 in E0 by PSCOMP_1:def 6;

E0 is real-bounded by RCOMP_1:10;

then E0 is bounded_below by XXREAL_2:def 11;

then |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `2 <= pp `2 by A14, A20, A35, SEQ_4:def 2;

then A36: pp `2 = |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `2 by A34, XXREAL_0:1;

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

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

end;reconsider E0 = proj2 .: EE as compact Subset of REAL by JCT_MISC:15;

A27: (Gauge (C,n)) * (i,j) in LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by RLTOPSP1:68;

A28: ((Gauge (C,n)) * (i,k)) `1 = |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `1 by A1, A2, A5, A7, A19, A20, GOBOARD5:2;

A29: |[(((Gauge (C,n)) * (i,1)) `1),(lower_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, A18, A20, SPRECT_3:12;

A30: ((Gauge (C,n)) * (i,j)) `2 <= |[(((Gauge (C,n)) * (i,1)) `1),(lower_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, A20, SPRECT_3:12;

((Gauge (C,n)) * (i,j)) `1 = |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `1 by A1, A2, A3, A11, A19, A20, GOBOARD5:2;

then |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| in LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by A28, A30, A29, GOBOARD7:7;

then A31: LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j))) c= LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) by A27, TOPREAL1:6;

assume A32: x in (LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) ; :: thesis: x = |[(((Gauge (C,n)) * (i,1)) `1),(lower_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) ;

A33: pp in LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j))) by A32, XBOOLE_0:def 4;

then A34: pp `2 <= |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `2 by A21, TOPREAL1:4;

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

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

then proj2 . pp in E0 by FUNCT_2:35;

then A35: pp `2 in E0 by PSCOMP_1:def 6;

E0 is real-bounded by RCOMP_1:10;

then E0 is bounded_below by XXREAL_2:def 11;

then |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `2 <= pp `2 by A14, A20, A35, SEQ_4:def 2;

then A36: pp `2 = |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]| `2 by A34, XXREAL_0:1;

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

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

then x in LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j))) by RLTOPSP1:68;

hence x in (LSeg (|[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) by A26, A37, XBOOLE_0:def 4; :: thesis: verum