let n be Nat; :: thesis:
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
let i, j, k be Nat; :: thesis:
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:
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:
thus ( j <= j1 & j1 <= k ) by A12, A13; :: thesis:
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

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

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:
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:

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~ (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: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:

end;

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: