let f be FinSequence of (TOP-REAL 2); ( 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)
; 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
;
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 Th7;
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 not LSeg (f,1) meets LSeg (f,((len f) -' 1))assume A12:
LSeg (
f,1)
meets LSeg (
f,
((len f) -' 1))
;
contradictionnow ( ( (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} & ( f . 1 = f . ((len f) -' 1) or f . 1 = f . (((len f) -' 1) + 1) ) & contradiction ) 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) ) & contradiction ) or ( LSeg (f,1) = LSeg (f,((len f) -' 1)) & contradiction ) )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;
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) ) )
;
contradictionnow ( ( f . (1 + 1) = f . ((len f) -' 1) & contradiction ) or ( f . (1 + 1) = f . (((len f) -' 1) + 1) & contradiction ) )end; hence
contradiction
;
verum end; case
LSeg (
f,1)
= LSeg (
f,
((len f) -' 1))
;
contradictionthen
LSeg (
(f /. 1),
(f /. (1 + 1)))
= LSeg (
f,
((len f) -' 1))
by A9, TOPREAL1:def 3;
then A14:
LSeg (
(f /. 1),
(f /. (1 + 1)))
= LSeg (
(f /. ((len f) -' 1)),
(f /. (((len f) -' 1) + 1)))
by A6, A10, TOPREAL1:def 3;
A15:
1
+ 1
< ((len f) -' 1) + 1
by A6, XREAL_1:6;
(len f) -' 1
< len f
by A11, NAT_1:13;
then A16:
f /. ((len f) -' 1) = f . ((len f) -' 1)
by A6, FINSEQ_4:15;
1
< len f
by A6, NAT_D:44;
then A17:
f /. 1
= f . 1
by FINSEQ_4:15;
A18:
(
f /. (1 + 1) = f . (1 + 1) &
f /. (((len f) -' 1) + 1) = f . (((len f) -' 1) + 1) )
by A7, A9, A10, FINSEQ_4:15;
hence
contradiction
;
verum end; end; end; hence
contradiction
;
verum end; hence
f is
s.n.c.
by A1, A2, Th13, Th14;
verum end; end;