let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is nodic & PairF f is Simple & f . 1 <> f . (len f) implies f is s.n.c. )
assume A1: ( f is nodic & PairF f is Simple & f . 1 <> f . (len f) ) ; :: thesis: f is s.n.c.
reconsider f1 = f as FinSequence of the carrier of (PGraph the carrier of (TOP-REAL 2)) ;
A2: (len f) -' 1 <= len f by NAT_D:44;

per cases ( (len f) -' 1 > 2 or (len f) -' 1 <= 2 ) ;

suppose A3: (len f) -' 1 > 2 ; :: thesis: f is s.n.c.

then A4: (len f) -' 1 > 1 by XXREAL_0:2;
then A5: 1 < len f by NAT_D:44;
len f >= 1 by A4, NAT_D:44;
then A6: f1 is_oriented_vertex_seq_of PairF f by Th11;
A7: 1 + 1 < len f by A3, NAT_D:44;
A8: (len f) -' 1 = (len f) - 1 by A4, NAT_D:39;
then A9: ((len f) -' 1) + 1 = len f ;

now

assume A10: LSeg f,1 meets LSeg f,((len f) -' 1) ; :: thesis: contradiction

now

per cases ( ( (LSeg f,1) /\ (LSeg f,((len f) -' 1)) = {(f . 1)} & ( f . 1 = f . ((len f) -' 1) or f . 1 = f . (((len f) -' 1) + 1) ) ) or ( (LSeg f,1) /\ (LSeg f,((len f) -' 1)) = {(f . (1 + 1))} & ( f . (1 + 1) = f . ((len f) -' 1) or f . (1 + 1) = f . (((len f) -' 1) + 1) ) ) or LSeg f,1 = LSeg f,((len f) -' 1) ) by A1, A10, Def4;

case ( (LSeg f,1) /\ (LSeg f,((len f) -' 1)) = {(f . 1)} & ( f . 1 = f . ((len f) -' 1) or f . 1 = f . (((len f) -' 1) + 1) ) ) ; :: thesis: contradiction

hence contradiction by A1, A2, A4, A6, A8, Th4; :: thesis: verum

end;

case A11: ( (LSeg f,1) /\ (LSeg f,((len f) -' 1)) = {(f . (1 + 1))} & ( f . (1 + 1) = f . ((len f) -' 1) or f . (1 + 1) = f . (((len f) -' 1) + 1) ) ) ; :: thesis: contradiction

now

per cases ( f . (1 + 1) = f . ((len f) -' 1) or f . (1 + 1) = f . (((len f) -' 1) + 1) ) by A11;

case f . (1 + 1) = f . ((len f) -' 1) ; :: thesis: contradiction

hence contradiction by A1, A2, A3, A6, Th4; :: thesis: verum

end;

case f . (1 + 1) = f . (((len f) -' 1) + 1) ; :: thesis: contradiction

hence contradiction by A1, A6, A7, A8, Th4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A12: LSeg f,1 = LSeg f,((len f) -' 1) ; :: thesis: contradiction

A13: 1 + 1 < ((len f) -' 1) + 1 by A4, XREAL_1:8;
A14: (len f) -' 1 < len f by A9, NAT_1:13;
A15: 1 < len f by A4, NAT_D:44;
LSeg (f /. 1),(f /. (1 + 1)) = LSeg f,((len f) -' 1) by A7, A12, TOPREAL1:def 5;
then A16: LSeg (f /. 1),(f /. (1 + 1)) = LSeg (f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1)) by A4, A8, TOPREAL1:def 5;
A17: f /. 1 = f . 1 by A15, FINSEQ_4:24;
A18: f /. (1 + 1) = f . (1 + 1) by A7, FINSEQ_4:24;
A19: f /. ((len f) -' 1) = f . ((len f) -' 1) by A4, A14, FINSEQ_4:24;
A20: f /. (((len f) -' 1) + 1) = f . (((len f) -' 1) + 1) by A5, A8, FINSEQ_4:24;

now

per cases ( ( f . 1 = f . ((len f) -' 1) & f . (1 + 1) = f . (((len f) -' 1) + 1) ) or ( f . 1 = f . (((len f) -' 1) + 1) & f . (1 + 1) = f . ((len f) -' 1) ) ) by A16, A17, A18, A19, A20, SPPOL_1:25;

case ( f . 1 = f . ((len f) -' 1) & f . (1 + 1) = f . (((len f) -' 1) + 1) ) ; :: thesis: contradiction

hence contradiction by A1, A6, A8, A13, Th4; :: thesis: verum

end;

case ( f . 1 = f . (((len f) -' 1) + 1) & f . (1 + 1) = f . ((len f) -' 1) ) ; :: thesis: contradiction

hence contradiction by A1, A8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence f is s.n.c. by A1, Th17, Th18; :: thesis: verum

end;

suppose A21: (len f) -' 1 <= 2 ; :: 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 A22: i + 1 < j ; :: thesis: LSeg f,i misses LSeg f,j

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

suppose A23: ( 1 <= i & j + 1 <= len f ) ; :: thesis: LSeg f,i misses LSeg f,j

(i + 1) + 1 < j + 1 by A22, XREAL_1:8;
then A24: (i + 1) + 1 < len f by A23, XXREAL_0:2;
1 < i + 1 by A23, NAT_1:13;
then 1 + 1 < (i + 1) + 1 by XREAL_1:10;
then (1 + 1) + 1 <= (i + 1) + 1 by NAT_1:13;
then (1 + 1) + 1 < len f by A24, XXREAL_0:2;
then A25: ((1 + 1) + 1) - 1 < (len f) - 1 by XREAL_1:11;
then 1 < (len f) - 1 by XXREAL_0:2;
hence LSeg f,i misses LSeg f,j by A21, A25, NAT_D:39; :: thesis: verum

end;

suppose A26: ( 1 > i or j + 1 > len f ) ; :: thesis: LSeg f,i misses LSeg f,j

now

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

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

end;

end;