let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Lower_Seq (C,n)) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i, j, k being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Lower_Seq (C,n)) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )
let i, j, k be Nat; :: thesis: ( 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Lower_Seq (C,n)) implies ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} ) )
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~ (Lower_Seq (C,n)) ; :: thesis: ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )
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,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~ (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 w1 = lower_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 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~ (Lower_Seq (C,n))))) by A4, A10, A8, JORDAN1F:1, JORDAN1G:5;
set p = |[(((Gauge (C,n)) * (i,1)) `1),(lower_bound (proj2 .: ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_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: ( j <= k1 & k1 <= k & (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} )
thus ( j <= k1 & k1 <= k ) by A12, A13; :: thesis: (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))}
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~ (Lower_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~ (Lower_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~ (Lower_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~ (Lower_Seq (C,n))) by A17, XBOOLE_0:def 4;
then A24: pp in L~ (Lower_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~ (Lower_Seq (C,n))))))]| `2 = S-bound ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_Seq (C,n)))) by A14, A20, SPRECT_1:44
.= (S-min ((LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (L~ (Lower_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~ (Lower_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~ (Lower_Seq (C,n))))))]| in L~ (Lower_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~ (Lower_Seq (C,n))))))]|,((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_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~ (Lower_Seq (C,n))))))]| ) hence (LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} by A20, TARSKI:def 1; :: thesis: verum