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 <= 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)) * (k,i) in L~ (Lower_Seq (C,n)) ; :: thesis:
set G = Gauge (C,n);
A7: k >= 1 by A1, A2, XXREAL_0:2;
then A8: [k,i] in Indices (Gauge (C,n)) by A3, A4, A5, MATRIX_0:30;
set X = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)));
A9: (Gauge (C,n)) * (k,i) in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by RLTOPSP1:68;
then reconsider X1 = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (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)) * (j,i)),((Gauge (C,n)) * (k,i))) meets L~ (Lower_Seq (C,n)) by A6, A9, XBOOLE_0:3;
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~ (Lower_Seq (C,n)))));
A11: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then A12: j <= width (Gauge (C,n)) by A2, A3, XXREAL_0:2;
then [j,i] in Indices (Gauge (C,n)) by A1, A4, A5, A11, MATRIX_0:30;
then consider k1 being Nat such that
A13: j <= k1 and
A14: k1 <= k and
A15: ((Gauge (C,n)) * (k1,i)) `1 = lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))))) by A2, A10, A8, JORDAN1F:3, JORDAN1G:5;
set p = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|;
A16: k1 <= width (Gauge (C,n)) by A3, A11, A14, XXREAL_0:2;
((Gauge (C,n)) * (j,i)) `2 = ((Gauge (C,n)) * (1,i)) `2 by A1, A4, A5, A11, A12, GOBOARD5:1
.= ((Gauge (C,n)) * (k,i)) `2 by A3, A4, A5, A7, GOBOARD5:1 ;
then A17: LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) is horizontal by SPPOL_1:15;
take k1 ; :: thesis:
thus ( j <= k1 & k1 <= k ) by A13, A14; :: thesis:
consider pp being object such that
A18: pp in W-most X1 by XBOOLE_0:def 1;
A19: 1 <= k1 by A1, A13, XXREAL_0:2;
then A20: ((Gauge (C,n)) * (k1,i)) `2 = ((Gauge (C,n)) * (1,i)) `2 by A4, A5, A11, A16, GOBOARD5:1;
then A21: |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| = (Gauge (C,n)) * (k1,i) by A15, EUCLID:53;
then A22: ((Gauge (C,n)) * (j,i)) `1 <= |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 by A1, A4, A5, A11, A13, A16, SPRECT_3:13;
A23: ((Gauge (C,n)) * (j,i)) `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2 by A1, A4, A5, A11, A12, A20, A21, GOBOARD5:1;
reconsider pp = pp as Point of (TOP-REAL 2) by A18;
A24: pp in (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))) by A18, XBOOLE_0:def 4;
then A25: pp in L~ (Lower_Seq (C,n)) by XBOOLE_0:def 4;
A26: |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 = W-bound ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))) by A15, A21, SPRECT_1:43
.= (W-min ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))))) `1 by EUCLID:52
.= pp `1 by A18, PSCOMP_1:31 ;
pp in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by A24, XBOOLE_0:def 4;
then pp `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2 by A23, A17, SPPOL_1:40;
then A27: |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| in L~ (Lower_Seq (C,n)) by A25, A26, TOPREAL3:6;
for x being object holds
( x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,((Gauge (C,n)) * (j,i)))) /\ (L~ (Lower_Seq (C,n))) iff x = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| )

proof

let x be object ; :: thesis:
thus ( x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,((Gauge (C,n)) * (j,i)))) /\ (L~ (Lower_Seq (C,n))) implies x = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| ) :: thesis:

proof

reconsider EE = (LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n))) as compact Subset of (TOP-REAL 2) ;
assume A28: x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,((Gauge (C,n)) * (j,i)))) /\ (L~ (Lower_Seq (C,n))) ; :: thesis:
then reconsider pp = x as Point of (TOP-REAL 2) ;
A29: pp in LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,((Gauge (C,n)) * (j,i))) by A28, XBOOLE_0:def 4;
then A30: pp `1 <= |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 by A22, TOPREAL1:3;
A31: |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 <= ((Gauge (C,n)) * (k,i)) `1 by A3, A4, A5, A14, A19, A21, SPRECT_3:13;
A32: ((Gauge (C,n)) * (j,i)) `1 <= |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 by A1, A4, A5, A11, A13, A16, A21, SPRECT_3:13;
A33: ((Gauge (C,n)) * (k,i)) `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2 by A3, A4, A5, A7, A20, A21, GOBOARD5:1;
reconsider E0 = proj1 .: EE as compact Subset of REAL by Th4;
A34: (Gauge (C,n)) * (j,i) in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by RLTOPSP1:68;
((Gauge (C,n)) * (j,i)) `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2 by A1, A4, A5, A11, A12, A20, A21, GOBOARD5:1;
then |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| in LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by A33, A32, A31, GOBOARD7:8;
then A35: LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,((Gauge (C,n)) * (j,i))) c= LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) by A34, TOPREAL1:6;
pp in L~ (Lower_Seq (C,n)) by A28, XBOOLE_0:def 4;
then pp in EE by A29, A35, XBOOLE_0:def 4;
then proj1 . pp in E0 by FUNCT_2:35;
then A36: 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~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 <= pp `1 by A15, A21, A36, SEQ_4:def 2;
then A37: pp `1 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `1 by A30, XXREAL_0:1;
pp `2 = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| `2 by A23, A29, GOBOARD7:6;
hence x = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| by A37, TOPREAL3:6; :: thesis:

end;

assume A38: x = |[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]| ; :: thesis:
then x in LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,((Gauge (C,n)) * (j,i))) by RLTOPSP1:68;
hence x in (LSeg (|[(lower_bound (proj1 .: ((LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i)))) /\ (L~ (Lower_Seq (C,n)))))),(((Gauge (C,n)) * (1,i)) `2)]|,((Gauge (C,n)) * (j,i)))) /\ (L~ (Lower_Seq (C,n))) by A27, A38, XBOOLE_0:def 4; :: thesis:

end;

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