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~ (Lower_Seq (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) holds
ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,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)) * (j,i) in L~ (Lower_Seq (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) holds
ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,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)) * (j,i) in L~ (Lower_Seq (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) implies ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,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)) * (j,i) in L~ (Lower_Seq (C,n)) and
A7: (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) ; :: thesis: ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )

set G = Gauge (C,n);
A8: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then A9: j <= width (Gauge (C,n)) by ;
then A10: [j,i] in Indices (Gauge (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: (Gauge (C,n)) * (k,i) in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by RLTOPSP1:68;
then A12: LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets L~ (Upper_Seq (C,n)) by ;
A13: k >= 1 by ;
then [k,i] in Indices (Gauge (C,n)) by ;
then consider k1 being Nat such that
A14: j <= k1 and
A15: k1 <= k and
A16: ((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 ;
A17: k1 <= width (Gauge (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)]|;
set w2 = upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))));
set q = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|;
A18: (Gauge (C,n)) * (j,i) in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i))) by RLTOPSP1:68;
then A19: LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i))) meets L~ (Lower_Seq (C,n)) by ;
A20: 1 <= k1 by ;
then A21: ((Gauge (C,n)) * (k1,i)) `2 = ((Gauge (C,n)) * (1,i)) `2 by ;
then A22: |[(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 ;
((Gauge (C,n)) * (j,i)) `2 = ((Gauge (C,n)) * (1,i)) `2 by A1, A4, A5, A8, A9, GOBOARD5:1
.= ((Gauge (C,n)) * (k,i)) `2 by ;
then A23: LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) is horizontal by SPPOL_1:15;
set X = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n)));
reconsider X1 = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) as non empty compact Subset of () by ;
consider pp being object such that
A24: pp in E-most X1 by XBOOLE_0:def 1;
[k1,i] in Indices (Gauge (C,n)) by ;
then consider j1 being Nat such that
A25: j <= j1 and
A26: j1 <= k1 and
A27: ((Gauge (C,n)) * (j1,i)) `1 = upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n))))) by ;
A28: j1 <= width (Gauge (C,n)) by ;
reconsider pp = pp as Point of () by A24;
A29: pp in (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) by ;
then A30: pp in L~ (Lower_Seq (C,n)) by XBOOLE_0:def 4;
take j1 ; :: thesis: ex k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )

take k1 ; :: thesis: ( j <= j1 & j1 <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
thus ( j <= j1 & j1 <= k1 & k1 <= k ) by ; :: thesis: ( (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} & (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} )
A31: pp in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i))) by ;
A32: 1 <= j1 by ;
then A33: ((Gauge (C,n)) * (j1,i)) `2 = ((Gauge (C,n)) * (1,i)) `2 by ;
then A34: |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| = (Gauge (C,n)) * (j1,i) by ;
then A35: |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `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 ;
A36: |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 = E-bound ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n)))) by
.= (E-min ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))))) `1 by EUCLID:52
.= pp `1 by ;
A37: ((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, A8, A9, A21, A22, GOBOARD5:1;
then LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|) is horizontal by SPPOL_1:15;
then pp `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2 by ;
then A38: |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| in L~ (Lower_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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n))) iff x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n))) iff x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n))) implies x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| ) :: thesis: ( x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n))) )
proof
reconsider EE = (LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n))) as compact Subset of () ;
assume A39: 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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n))) ; :: thesis: x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|
then reconsider pp = x as Point of () ;
A40: 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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|) by ;
then A41: pp `1 >= |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 by ;
A42: ((Gauge (C,n)) * (j,i)) `1 <= |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 by A1, A4, A5, A8, A25, A28, A34, SPRECT_3:13;
reconsider E0 = proj1 .: EE as compact Subset of REAL by Th4;
A43: |[(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)),|[(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 RLTOPSP1:68;
((Gauge (C,n)) * (j,i)) `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2 by A1, A4, A5, A8, A9, A33, A34, GOBOARD5:1;
then |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| 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 A44: 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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|) c= LSeg (((Gauge (C,n)) * (j,i)),|[(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 ;
pp in L~ (Lower_Seq (C,n)) by ;
then pp in EE by ;
then proj1 . pp in E0 by FUNCT_2:35;
then A45: 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)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 >= pp `1 by ;
then A46: pp `1 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 by ;
pp `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2 by ;
hence x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| by ; :: thesis: verum
end;
assume A47: x = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|) 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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Lower_Seq (C,n))) by ; :: thesis: verum
end;
hence (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (j1,i))} by ; :: thesis: (LSeg (((Gauge (C,n)) * (j1,i)),((Gauge (C,n)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))}
set X = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n)));
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 ;
consider pp being object such that
A48: pp in W-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of () by A48;
A49: pp in (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Upper_Seq (C,n))) by ;
then A50: pp in L~ (Upper_Seq (C,n)) by XBOOLE_0:def 4;
pp in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by ;
then A51: 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 ;
|[(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 ;
then A52: |[(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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (L~ (Upper_Seq (C,n))) )
proof
j1 <= k by ;
then A53: |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 <= ((Gauge (C,n)) * (k,i)) `1 by ;
A54: ((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 ;
A55: ((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 A1, A4, A5, A8, A14, A17, A22, SPRECT_3:13;
A56: ((Gauge (C,n)) * (j,i)) `1 <= |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 by A1, A4, A5, A8, A25, A28, A34, SPRECT_3:13;
A57: |[(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 ;
((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, A8, A9, A21, A22, GOBOARD5:1;
then A58: |[(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 ;
A59: ((Gauge (C,n)) * (k,i)) `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2 by ;
((Gauge (C,n)) * (j,i)) `2 = |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2 by A1, A4, A5, A8, A9, A33, A34, GOBOARD5:1;
then |[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by ;
then A60: 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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_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 A61: 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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (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 () ;
A62: 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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|) by ;
then A63: 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 in L~ (Upper_Seq (C,n)) by ;
then pp in EE by ;
then proj1 . pp in E0 by FUNCT_2:35;
then A64: 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 A65: 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 A66: 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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|)) /\ (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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|) 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)]|,|[(upper_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),|[(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)]|)) /\ (L~ (Lower_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)) * (k1,i)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (k1,i))} by ; :: thesis: verum