let f be FinSequence of (); :: 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 ;
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 ;
then LSeg (f,i) misses LSeg (f,j) by ;
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