let p, p1, p2 be Point of (TOP-REAL 2); :: thesis:
let f be non constant standard special_circular_sequence; :: thesis:
assume A1: (L~ f) /\ (LSeg p1,p2) = {p} ; :: thesis:
let r be Point of (TOP-REAL 2); :: thesis:
assume that
A2: not r in LSeg p1,p2 and
A3: ( not p1 in L~ f & not p2 in L~ f ) and
A4: ( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) ) and
A5: ex i being Element of 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 ) and
A6: not r in L~ f ; :: thesis:
A7: f is_sequence_on GoB f by GOBOARD5:def 5;
consider i being Element of NAT such that
A8: ( 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 ) by A5;
A9: LSeg f,i c= left_cell f,i,(GoB f) by A7, A8, JORDAN1H:26;
A10: LSeg f,i c= right_cell f,i,(GoB f) by A7, A8, JORDAN1H:28;
A11: p in (L~ f) /\ (LSeg p1,p2) by A1, TARSKI:def 1;
then A12: ( p <> p2 & p <> p1 ) by A3, XBOOLE_0:def 4;
A13: p in LSeg p1,p2 by A11, XBOOLE_0:def 4;
A14: right_cell f,i,(GoB f) is convex by A8, Th23;
A15: left_cell f,i,(GoB f) is convex by A8, Th23;
A16: (right_cell f,i,(GoB f)) \ (L~ f) c= RightComp f by A7, A8, JORDAN9:29;
A17: (left_cell f,i,(GoB f)) \ (L~ f) c= LeftComp f by A7, A8, JORDAN9:29;

A18: now

assume r in right_cell f,i,(GoB f) ; :: thesis:
then r in (right_cell f,i,(GoB f)) \ (L~ f) by A6, XBOOLE_0:def 5;
hence r in RightComp f by A16; :: thesis:

end;

A19: now

assume r in left_cell f,i,(GoB f) ; :: thesis:
then r in (left_cell f,i,(GoB f)) \ (L~ f) by A6, XBOOLE_0:def 5;
hence r in LeftComp f by A17; :: thesis:

end;

A20: now

assume A21: ( p1 in LSeg r,p & r in right_cell f,i,(GoB f) ) ; :: thesis:
then LSeg r,p c= right_cell f,i,(GoB f) by A8, A10, A14, JORDAN1:def 1;
then p1 in (right_cell f,i,(GoB f)) \ (L~ f) by A3, A21, XBOOLE_0:def 5;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) by A16, A18, A21, Th15; :: thesis:

end;

A22: now

assume A23: ( p1 in LSeg r,p & r in left_cell f,i,(GoB f) ) ; :: thesis:
then LSeg r,p c= left_cell f,i,(GoB f) by A8, A9, A15, JORDAN1:def 1;
then p1 in (left_cell f,i,(GoB f)) \ (L~ f) by A3, A23, XBOOLE_0:def 5;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) by A17, A19, A23, Th15; :: thesis:

end;

A24: now

assume A25: ( p2 in LSeg r,p & r in right_cell f,i,(GoB f) ) ; :: thesis:
then LSeg r,p c= right_cell f,i,(GoB f) by A8, A10, A14, JORDAN1:def 1;
then p2 in (right_cell f,i,(GoB f)) \ (L~ f) by A3, A25, XBOOLE_0:def 5;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) by A16, A18, A25, Th15; :: thesis:

end;

A26: now

assume A27: ( p2 in LSeg r,p & r in left_cell f,i,(GoB f) ) ; :: thesis:
then LSeg r,p c= left_cell f,i,(GoB f) by A8, A9, A15, JORDAN1:def 1;
then p2 in (left_cell f,i,(GoB f)) \ (L~ f) by A3, A27, XBOOLE_0:def 5;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) by A17, A19, A27, Th15; :: thesis:

end;

per cases by A2, A4, A12, A13, Th29;

suppose A28: p1 in LSeg r,p ; :: thesis:

per cases by A8;

suppose r in right_cell f,i,(GoB f) ; :: thesis:

hence ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) ) by A20, A28; :: thesis:

end;

suppose r in left_cell f,i,(GoB f) ; :: thesis:

end;

hence ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) ) ; :: thesis:

end;

suppose A29: p2 in LSeg r,p ; :: thesis:

per cases by A8;

suppose r in right_cell f,i,(GoB f) ; :: thesis:

end;

suppose r in left_cell f,i,(GoB f) ; :: thesis:

end;