let C be Simple_closed_curve; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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;

p1,p2 are_neighbours_wrt q,q,C

let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( 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 ) ; :: thesis: 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;

per cases
( ( q in P1 & not q in P2 ) or ( q in P2 & not q in P1 ) or ( q in P1 & q in P2 ) )
by A1, A6, XBOOLE_0:def 3;

end;

suppose A8:
( q in P1 & not q in P2 )
; :: thesis: p1,p2 are_neighbours_wrt q,q,C

take
P2
; :: according to JORDAN18:def 3 :: thesis: ( P2 is_an_arc_of p1,p2 & P2 c= C & not P2 meets {q,q} )

thus P2 is_an_arc_of p1,p2 by A5; :: thesis: ( P2 c= C & not P2 meets {q,q} )

thus P2 c= C by A6, XBOOLE_1:7; :: thesis: not P2 meets {q,q}

thus P2 misses {q,q} by A8, ZFMISC_1:51; :: thesis: verum

end;thus P2 is_an_arc_of p1,p2 by A5; :: thesis: ( P2 c= C & not P2 meets {q,q} )

thus P2 c= C by A6, XBOOLE_1:7; :: thesis: not P2 meets {q,q}

thus P2 misses {q,q} by A8, ZFMISC_1:51; :: thesis: verum

suppose A9:
( q in P2 & not q in P1 )
; :: thesis: p1,p2 are_neighbours_wrt q,q,C

take
P1
; :: according to JORDAN18:def 3 :: thesis: ( P1 is_an_arc_of p1,p2 & P1 c= C & not P1 meets {q,q} )

thus P1 is_an_arc_of p1,p2 by A4; :: thesis: ( P1 c= C & not P1 meets {q,q} )

thus P1 c= C by A6, XBOOLE_1:7; :: thesis: not P1 meets {q,q}

thus P1 misses {q,q} by A9, ZFMISC_1:51; :: thesis: verum

end;thus P1 is_an_arc_of p1,p2 by A4; :: thesis: ( P1 c= C & not P1 meets {q,q} )

thus P1 c= C by A6, XBOOLE_1:7; :: thesis: not P1 meets {q,q}

thus P1 misses {q,q} by A9, ZFMISC_1:51; :: thesis: verum

suppose
( q in P1 & q in P2 )
; :: thesis: p1,p2 are_neighbours_wrt q,q,C

then
q in P1 /\ P2
by XBOOLE_0:def 4;

hence p1,p2 are_neighbours_wrt q,q,C by A3, A7, TARSKI:def 2; :: thesis: verum

end;hence p1,p2 are_neighbours_wrt q,q,C by A3, A7, TARSKI:def 2; :: thesis: verum