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)
A4: ( i in NAT & j in NAT ) by ORDINAL1:def 12;

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

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

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

now

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

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

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

now

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

case A8: ( 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, A5, A8, XREAL_1:233;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} by XBOOLE_0:def 7; :: 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 A6, XXREAL_0:1;
then LSeg (f,i) misses LSeg (f,j) by A1, A3, A4, A7, GOBOARD5:def 4;
hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} by XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

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

end;

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

now

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

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) by XBOOLE_0:def 7; :: thesis: verum

end;

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

now

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

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

i + 1 > len f by A10;
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) by XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

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