let C be Simple_closed_curve; for p1, p2, q being Point of (TOP-REAL 2) st q in C & p1 in C & p2 in C & p1 <> p2 & p1 <> q & p2 <> q holds
p1,p2 are_neighbours_wrt q,q,C
let p1, p2, q be Point of (TOP-REAL 2); ( q in C & p1 in C & p2 in C & p1 <> p2 & p1 <> q & p2 <> q implies p1,p2 are_neighbours_wrt q,q,C )
assume that
A1:
q in C
and
A2:
( p1 in C & p2 in C & p1 <> p2 )
and
A3:
( p1 <> q & p2 <> q )
; p1,p2 are_neighbours_wrt q,q,C
consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A4:
P1 is_an_arc_of p1,p2
and
A5:
P2 is_an_arc_of p1,p2
and
A6:
C = P1 \/ P2
and
A7:
P1 /\ P2 = {p1,p2}
by A2, TOPREAL2:5;