let n be Element of NAT ; :: thesis:
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
let i, j, k be Element of NAT ; :: thesis:
assume that
A1: ( 1 <= i & i <= len (Gauge C,n) ) and
A2: ( 1 <= j & j <= k & k <= width (Gauge C,n) ) and
A3: (Gauge C,n) * i,j in L~ (Lower_Seq C,n) ; :: thesis:
set G = Gauge C,n;
set s = ((Gauge C,n) * i,1) `1 ;
set f = (Gauge C,n) * i,j;
set e = (Gauge C,n) * i,k;
set w2 = upper_bound (proj2 .: ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n))));
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)))))]|;
A4: j <= width (Gauge C,n) by A2, XXREAL_0:2;
then A5: [i,j] in Indices (Gauge C,n) by A1, A2, MATRIX_1:37;
A6: k >= 1 by A2, XXREAL_0:2;
then A7: ((Gauge C,n) * i,k) `1 = ((Gauge C,n) * i,1) `1 by A1, A2, GOBOARD5:3;
A8: Lower_Seq C,n is_sequence_on Gauge C,n by JORDAN1G:5;
A9: (Gauge C,n) * i,j in LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) by RLTOPSP1:69;
then A10: LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets L~ (Lower_Seq C,n) by A3, XBOOLE_0:3;
[i,k] in Indices (Gauge C,n) by A1, A2, A6, MATRIX_1:37;
then consider j1 being Element of NAT such that
A11: ( j <= j1 & j1 <= k ) and
A12: ((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 A2, A5, A8, A10, JORDAN1F:2;
A13: ( 1 <= j1 & j1 <= width (Gauge C,n) ) by A2, A11, XXREAL_0:2;
then A14: ((Gauge C,n) * i,j1) `1 = ((Gauge C,n) * i,1) `1 by A1, GOBOARD5:3;
then A15: |[(((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 A12, EUCLID:57;
take j1 ; :: thesis:
thus ( j <= j1 & j1 <= k ) by A11; :: thesis:
A16: |[(((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, A11, A13, A15, SPRECT_3:24;
set X = (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n));
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 A3, A9, PSCOMP_1:64, XBOOLE_0:def 4;
consider pp being set such that
A17: pp in N-most X1 by XBOOLE_0:def 1;
reconsider pp = pp as Point of (TOP-REAL 2) by A17;
A18: 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 A19: pp in L~ (Lower_Seq C,n) by XBOOLE_0:def 4;
A20: pp in LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) by A18, XBOOLE_0:def 4;
((Gauge C,n) * i,j) `1 = ((Gauge C,n) * i,k) `1 by A1, A2, A4, A7, GOBOARD5:3;
then LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) is vertical by SPPOL_1:37;
then A21: 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 A7, A14, A15, A20, SPPOL_1:64;
|[(((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 A12, A15, SPRECT_1:50
.= (N-min ((LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)))) `2 by EUCLID:56
.= pp `2 by A17, PSCOMP_1:98 ;
then A22: |[(((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 A19, A21, TOPREAL3:11;
for x being set 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

let x be set ; :: thesis:
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:

proof

assume A23: 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:
then reconsider pp = x as Point of (TOP-REAL 2) ;
A24: 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 A23, XBOOLE_0:def 4;
then A25: 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 A7, A14, A15, GOBOARD7:5;
A26: 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 A16, A24, TOPREAL1:10;
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) by PSCOMP_1:64;
reconsider E0 = proj2 .: EE as compact Subset of REAL by JCT_MISC:24;
A27: ((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, A4, A14, A15, GOBOARD5:3;
((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, A11, A13, A15, SPRECT_3:24;
then A28: |[(((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 A7, A14, A15, A16, A27, GOBOARD7:8;
(Gauge C,n) * i,k in LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) by RLTOPSP1:69;
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 A28, TOPREAL1:12;
E0 is bounded by RCOMP_1:28;
then A30: E0 is bounded_above by XXREAL_2:def 11;
pp in L~ (Lower_Seq C,n) by A23, XBOOLE_0:def 4;
then pp in EE by A24, A29, XBOOLE_0:def 4;
then proj2 . pp in E0 by FUNCT_2:43;
then pp `2 in E0 by PSCOMP_1:def 29;
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 A12, A15, A30, SEQ_4:def 4;
then 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 A26, XXREAL_0:1;
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 A25, TOPREAL3:11; :: thesis:

end;

assume A31: 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:
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:69;
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 A22, A31, XBOOLE_0:def 4; :: thesis:

end;

hence (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j1)} by A15, TARSKI:def 1; :: thesis: