let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of ()
for i being Nat st 1 <= i & i < len (Gauge (C,n)) holds
not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in L~ (Lower_Seq (C,n))

let C be connected compact non horizontal non vertical Subset of (); :: thesis: for i being Nat st 1 <= i & i < len (Gauge (C,n)) holds
not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in L~ (Lower_Seq (C,n))

set wi = width (Gauge (C,n));
let i be Nat; :: thesis: ( 1 <= i & i < len (Gauge (C,n)) implies not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in L~ (Lower_Seq (C,n)) )
assume that
A1: ( 1 <= i & i < len (Gauge (C,n)) ) and
A2: (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in L~ (Lower_Seq (C,n)) ; :: thesis: contradiction
set Gi1 = (Gauge (C,n)) * (i,(width (Gauge (C,n))));
consider ii being Nat such that
A3: 1 <= ii and
A4: ii + 1 <= len (Lower_Seq (C,n)) and
A5: (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in LSeg ((Lower_Seq (C,n)),ii) by ;
A6: LSeg ((Lower_Seq (C,n)),ii) = LSeg (((Lower_Seq (C,n)) /. ii),((Lower_Seq (C,n)) /. (ii + 1))) by ;
ii + 1 >= 1 by NAT_1:11;
then A7: ii + 1 in dom (Lower_Seq (C,n)) by ;
len (Gauge (C,n)) >= 4 by JORDAN8:10;
then ( len (Gauge (C,n)) = width (Gauge (C,n)) & len (Gauge (C,n)) > 1 ) by ;
then A8: [i,(width (Gauge (C,n)))] in Indices (Gauge (C,n)) by ;
ii < len (Lower_Seq (C,n)) by ;
then A9: ii in dom (Lower_Seq (C,n)) by ;
A10: not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Lower_Seq (C,n)) by ;
Lower_Seq (C,n) is_sequence_on Gauge (C,n) by Th5;
then consider i1, j1, i2, j2 being Nat such that
A11: [i1,j1] in Indices (Gauge (C,n)) and
A12: (Lower_Seq (C,n)) /. ii = (Gauge (C,n)) * (i1,j1) and
A13: [i2,j2] in Indices (Gauge (C,n)) and
A14: (Lower_Seq (C,n)) /. (ii + 1) = (Gauge (C,n)) * (i2,j2) and
A15: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by ;
A16: 1 <= i1 by ;
A17: j2 <= width (Gauge (C,n)) by ;
A18: 1 <= j1 by ;
A19: i1 <= len (Gauge (C,n)) by ;
A20: 1 <= j2 by ;
A21: i2 <= len (Gauge (C,n)) by ;
A22: 1 <= i2 by ;
A23: j1 <= width (Gauge (C,n)) by ;
per cases ( ( i1 = i2 & j2 + 1 = j1 ) or ( i2 + 1 = i1 & j1 = j2 ) or ( i2 = i1 + 1 & j1 = j2 ) or ( i1 = i2 & j2 = j1 + 1 ) ) by A15;
suppose A24: ( i1 = i2 & j2 + 1 = j1 ) ; :: thesis: contradiction
then j1 >= j2 by NAT_1:11;
then ((Gauge (C,n)) * (i1,j1)) `2 >= ((Gauge (C,n)) * (i2,j2)) `2 by ;
then A25: ((Gauge (C,n)) * (i1,j1)) `2 >= ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 by ;
((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (i2,1)) `1 by
.= ((Gauge (C,n)) * (i2,j2)) `1 by ;
then LSeg (((Lower_Seq (C,n)) /. ii),((Lower_Seq (C,n)) /. (ii + 1))) is vertical by ;
then ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `1 = ((Gauge (C,n)) * (i1,j1)) `1 by ;
then A26: i1 = i by A11, A8, Th7;
then ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 >= ((Gauge (C,n)) * (i1,j1)) `2 by ;
then j1 = width (Gauge (C,n)) by ;
hence contradiction by A12, A9, A10, A26, PARTFUN2:2; :: thesis: verum
end;
suppose A27: ( i2 + 1 = i1 & j1 = j2 ) ; :: thesis: contradiction
then ((Gauge (C,n)) * (i1,j1)) `2 = ((Gauge (C,n)) * (1,j2)) `2 by
.= ((Gauge (C,n)) * (i2,j2)) `2 by ;
then LSeg (((Lower_Seq (C,n)) /. ii),((Lower_Seq (C,n)) /. (ii + 1))) is horizontal by ;
then ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 = ((Gauge (C,n)) * (i1,j1)) `2 by ;
then A28: j1 = width (Gauge (C,n)) by A11, A8, Th6;
i2 < len (Gauge (C,n)) by ;
then not (Lower_Seq (C,n)) /. (ii + 1) in rng (Lower_Seq (C,n)) by A14, A22, A27, A28, Th43;
hence contradiction by A7, PARTFUN2:2; :: thesis: verum
end;
suppose A29: ( i2 = i1 + 1 & j1 = j2 ) ; :: thesis: contradiction
then ((Gauge (C,n)) * (i1,j1)) `2 = ((Gauge (C,n)) * (1,j2)) `2 by
.= ((Gauge (C,n)) * (i2,j2)) `2 by ;
then LSeg (((Lower_Seq (C,n)) /. ii),((Lower_Seq (C,n)) /. (ii + 1))) is horizontal by ;
then ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 = ((Gauge (C,n)) * (i1,j1)) `2 by ;
then A30: j1 = width (Gauge (C,n)) by A11, A8, Th6;
i1 < len (Gauge (C,n)) by ;
then not (Lower_Seq (C,n)) /. ii in rng (Lower_Seq (C,n)) by ;
hence contradiction by A9, PARTFUN2:2; :: thesis: verum
end;
suppose A31: ( i1 = i2 & j2 = j1 + 1 ) ; :: thesis: contradiction
then j2 >= j1 by NAT_1:11;
then ((Gauge (C,n)) * (i2,j2)) `2 >= ((Gauge (C,n)) * (i1,j1)) `2 by ;
then A32: ((Gauge (C,n)) * (i2,j2)) `2 >= ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 by ;
((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (i2,1)) `1 by
.= ((Gauge (C,n)) * (i2,j2)) `1 by ;
then LSeg (((Lower_Seq (C,n)) /. ii),((Lower_Seq (C,n)) /. (ii + 1))) is vertical by ;
then ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `1 = ((Gauge (C,n)) * (i1,j1)) `1 by ;
then A33: i1 = i by A11, A8, Th7;
then ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 >= ((Gauge (C,n)) * (i2,j2)) `2 by ;
then j2 = width (Gauge (C,n)) by ;
hence contradiction by A14, A7, A10, A31, A33, PARTFUN2:2; :: thesis: verum
end;
end;