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 that
A1: f is nodic and
A2: PairF f is Simple and
A3: 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)) ;
A4: (len f) -' 1 <= len f by NAT_D:44;

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

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

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

now

assume A12: 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, A12, 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 A2, A3, A4, A6, A8, A10, Th4; :: thesis: verum

end;

case A13: ( (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 A13;

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

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

end;

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

hence contradiction by A2, A8, A9, A10, Th4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

then LSeg (f /. 1),(f /. (1 + 1)) = LSeg f,((len f) -' 1) by A9, TOPREAL1:def 5;
then A14: LSeg (f /. 1),(f /. (1 + 1)) = LSeg (f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1)) by A6, A10, TOPREAL1:def 5;
A15: 1 + 1 < ((len f) -' 1) + 1 by A6, XREAL_1:8;
(len f) -' 1 < len f by A11, NAT_1:13;
then A16: f /. ((len f) -' 1) = f . ((len f) -' 1) by A6, FINSEQ_4:24;
1 < len f by A6, NAT_D:44;
then A17: f /. 1 = f . 1 by FINSEQ_4:24;
A18: ( f /. (1 + 1) = f . (1 + 1) & f /. (((len f) -' 1) + 1) = f . (((len f) -' 1) + 1) ) by A7, A9, A10, 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 A14, A17, A16, A18, SPPOL_1:25;

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

hence contradiction by A2, A8, A10, A15, Th4; :: thesis: verum

end;

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

hence contradiction by A3, A10; :: 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, A2, Th17, Th18; :: thesis: verum

end;

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

then 1 < i + 1 by NAT_1:13;
then 1 + 1 < (i + 1) + 1 by XREAL_1:10;
then A22: (1 + 1) + 1 <= (i + 1) + 1 by NAT_1:13;
(i + 1) + 1 < j + 1 by A20, XREAL_1:8;
then (i + 1) + 1 < len f by A21, XXREAL_0:2;
then (1 + 1) + 1 < len f by A22, XXREAL_0:2;
then A23: ((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 A19, A23, NAT_D:39; :: thesis: verum

end;

suppose A24: ( 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 A24;

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;