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,k) in L~ (Upper_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~ (Upper_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~ (Upper_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~ (Upper_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~ (Upper_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~ (Upper_Seq (C,n))))) by A4, A10, A8, JORDAN1F:1, JORDAN1G:4;
set p = |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_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:
thus ( j <= k1 & k1 <= k ) by A12, A13; :: thesis:
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~ (Upper_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~ (Upper_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~ (Upper_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~ (Upper_Seq (C,n))) by A17, XBOOLE_0:def 4;
then A24: pp in L~ (Upper_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~ (Upper_Seq (C,n))))))]| `2 = S-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n)))) by A14, A20, SPRECT_1:44
.= (S-min ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_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~ (Upper_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~ (Upper_Seq (C,n))))))]| in L~ (Upper_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~ (Upper_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Upper_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~ (Upper_Seq (C,n))))))]| )

proof

let x be object ; :: thesis:
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~ (Upper_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Upper_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~ (Upper_Seq (C,n))))))]| ) :: thesis:

proof

reconsider EE = (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_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~ (Upper_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~ (Upper_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~ (Upper_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~ (Upper_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~ (Upper_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~ (Upper_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~ (Upper_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Upper_Seq (C,n))) ; :: thesis:
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~ (Upper_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~ (Upper_Seq (C,n))))))]| `2 by A21, TOPREAL1:4;
pp in L~ (Upper_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~ (Upper_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~ (Upper_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~ (Upper_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~ (Upper_Seq (C,n))))))]| by A36, TOPREAL3:6; :: thesis:

end;

assume A37: x = |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Upper_Seq (C,n))))))]| ; :: thesis:
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~ (Upper_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~ (Upper_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Upper_Seq (C,n))) by A26, A37, XBOOLE_0:def 4; :: thesis:

end;

hence (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} by A20, TARSKI:def 1; :: thesis: