let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is s.c.c. & LSeg (f,1) misses LSeg (f,((len f) -' 1)) implies f is s.n.c. )
assume that
A1: f is s.c.c. and
A2: LSeg (f,1) misses LSeg (f,((len f) -' 1)) ; :: thesis: f is s.n.c.
for i, j being Nat st i + 1 < j holds
LSeg (f,i) misses LSeg (f,j)

proof

let i, j be Nat; :: thesis: ( i + 1 < j implies LSeg (f,i) misses LSeg (f,j) )
assume A3: i + 1 < j ; :: thesis: LSeg (f,i) misses LSeg (f,j)

per cases ( len f <> 0 or len f = 0 ) ;

suppose len f <> 0 ; :: thesis: LSeg (f,i) misses LSeg (f,j)

then A4: len f >= 0 + 1 by NAT_1:13;

now :: thesis: ( ( 1 <= i & j + 1 <= len f & (LSeg (f,i)) /\ (LSeg (f,j)) = {} ) or ( ( not 1 <= i or not j + 1 <= len f ) & (LSeg (f,i)) /\ (LSeg (f,j)) = {} ) )

per cases ( ( 1 <= i & j + 1 <= len f ) or not 1 <= i or not j + 1 <= len f ) ;

case A5: ( 1 <= i & j + 1 <= len f ) ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,j)) = {}

then A6: j < len f by NAT_1:13;

now :: thesis: ( ( i = 1 & j + 1 = len f & (LSeg (f,i)) /\ (LSeg (f,j)) = {} ) or ( ( not i = 1 or not j + 1 = len f ) & (LSeg (f,i)) /\ (LSeg (f,j)) = {} ) )

per cases ( ( i = 1 & j + 1 = len f ) or not i = 1 or not j + 1 = len f ) ;

case A7: ( i = 1 & j + 1 = len f ) ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,j)) = {}

then j = (len f) - 1 ;
then LSeg (f,i) misses LSeg (f,j) by A2, A4, A7, XREAL_1:233;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: thesis: verum

end;

case ( not i = 1 or not j + 1 = len f ) ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,j)) = {}

then ( i > 1 or j + 1 < len f ) by A5, XXREAL_0:1;
then LSeg (f,i) misses LSeg (f,j) by A1, A3, A6, GOBOARD5:def 4;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: thesis: verum

end;

end;

end;

hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: thesis: verum

end;

case A8: ( not 1 <= i or not j + 1 <= len f ) ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,j)) = {}

now :: thesis: ( ( 1 > i & (LSeg (f,i)) /\ (LSeg (f,j)) = {} ) or ( j + 1 > len f & (LSeg (f,i)) /\ (LSeg (f,j)) = {} ) )

per cases ( 1 > i or j + 1 > len f ) by A8;

case 1 > i ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,j)) = {}

then LSeg (f,i) = {} by TOPREAL1:def 3;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: thesis: verum

end;

case j + 1 > len f ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,j)) = {}

then LSeg (f,j) = {} by TOPREAL1:def 3;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: thesis: verum

end;

end;

end;

hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: thesis: verum

end;

end;

end;

hence LSeg (f,i) misses LSeg (f,j) ; :: thesis: verum

end;

suppose A9: len f = 0 ; :: thesis: LSeg (f,i) misses LSeg (f,j)

now :: thesis: ( ( i >= 1 & (LSeg (f,i)) /\ (LSeg (f,j)) = {} ) or ( i < 1 & (LSeg (f,i)) /\ (LSeg (f,j)) = {} ) )

per cases ( i >= 1 or i < 1 ) ;

case i >= 1 ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,j)) = {}

i + 1 > len f by A9;
then LSeg (f,i) = {} by TOPREAL1:def 3;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: thesis: verum

end;

case i < 1 ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,j)) = {}

then LSeg (f,i) = {} by TOPREAL1:def 3;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: thesis: verum

end;

end;

end;

hence LSeg (f,i) misses LSeg (f,j) ; :: thesis: verum

end;

end;

end;

hence f is s.n.c. by TOPREAL1:def 7; :: thesis: verum