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 13;

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:235;
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 5;
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 5;
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 5;
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 5;
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 9; :: thesis: verum