for p, p1, p2 being Point of (TOP-REAL 2)
for f being non constant standard special_circular_sequence st (L~ f) /\ (LSeg (p1,p2)) = {p} holds
for r being Point of (TOP-REAL 2) st not r in LSeg (p1,p2) & not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len f & ( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) ) & p in LSeg (f,i) ) & not r in L~ f & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not r in C or not p1 in C ) ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C )