:: deftheorem Def3 defines Segmentation JORDAN_A:def 3 :
for C being Simple_closed_curve
for b₂ being FinSequence of (TOP-REAL 2) holds
( b₂ is Segmentation of C iff ( b₂ /. 1 = W-min C & b₂ is one-to-one & 8 <= len b₂ & rng b₂ c= C & ( for i being Nat st 1 <= i & i < len b₂ holds
LE b₂ /. i,b₂ /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len b₂ holds
(Segment ((b₂ /. i),(b₂ /. (i + 1)),C)) /\ (Segment ((b₂ /. (i + 1)),(b₂ /. (i + 2)),C)) = {(b₂ /. (i + 1))} ) & (Segment ((b₂ /. (len b₂)),(b₂ /. 1),C)) /\ (Segment ((b₂ /. 1),(b₂ /. 2),C)) = {(b₂ /. 1)} & (Segment ((b₂ /. ((len b₂) -' 1)),(b₂ /. (len b₂)),C)) /\ (Segment ((b₂ /. (len b₂)),(b₂ /. 1),C)) = {(b₂ /. (len b₂))} & Segment ((b₂ /. ((len b₂) -' 1)),(b₂ /. (len b₂)),C) misses Segment ((b₂ /. 1),(b₂ /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len b₂ & i,j aren't_adjacent holds
Segment ((b₂ /. i),(b₂ /. (i + 1)),C) misses Segment ((b₂ /. j),(b₂ /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len b₂ holds
Segment ((b₂ /. (len b₂)),(b₂ /. 1),C) misses Segment ((b₂ /. i),(b₂ /. (i + 1)),C) ) ) );