let C be Simple_closed_curve; :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1 in C & p2 in C & q1 in C & p1 <> p2 & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & not p1,p2 are_neighbours_wrt q1,q2,C holds
p1,q1 are_neighbours_wrt p2,q2,C
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( p1 in C & p2 in C & q1 in C & p1 <> p2 & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & not p1,p2 are_neighbours_wrt q1,q2,C implies p1,q1 are_neighbours_wrt p2,q2,C )
assume that
A1: ( p1 in C & p2 in C ) and
A2: q1 in C and
A3: p1 <> p2 and
A4: q1 <> p1 and
A5: q1 <> p2 and
A6: ( q2 <> p1 & q2 <> p2 ) ; :: thesis: ( p1,p2 are_neighbours_wrt q1,q2,C or p1,q1 are_neighbours_wrt p2,q2,C )
consider P, P1 being non empty Subset of (TOP-REAL 2) such that
A7: P is_an_arc_of p1,p2 and
A8: P1 is_an_arc_of p1,p2 and
A9: C = P \/ P1 and
A10: P /\ P1 = {p1,p2} by A1, A3, TOPREAL2:5;
A11: P c= C by A9, XBOOLE_1:7;
assume A12: for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C holds
A meets {q1,q2} ; :: according to JORDAN18:def 3 :: thesis: p1,q1 are_neighbours_wrt p2,q2,C
then A13: P meets {q1,q2} by A7, A9, XBOOLE_1:7;
A14: P1 c= C by A9, XBOOLE_1:7;

per cases ( ( q1 in P & not q2 in P ) or ( q2 in P & not q1 in P ) or ( q1 in P & q2 in P ) ) by A13, ZFMISC_1:51;

suppose that A15: q1 in P and
A16: not q2 in P ; :: thesis: p1,q1 are_neighbours_wrt p2,q2,C

now :: thesis: ex A being Element of bool the carrier of (TOP-REAL 2) st
( A is_an_arc_of p1,q1 & A c= C & A misses {p2,q2} )

take A = Segment (P,p1,p2,p1,q1); :: thesis: ( A is_an_arc_of p1,q1 & A c= C & A misses {p2,q2} )

A17: now :: thesis: not p2 in A

A18: A = { q where q is Point of (TOP-REAL 2) : ( LE p1,q,P,p1,p2 & LE q,q1,P,p1,p2 ) } by JORDAN6:26;
assume p2 in A ; :: thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( p2 = q & LE p1,q,P,p1,p2 & LE q,q1,P,p1,p2 ) by A18;
hence contradiction by A5, A7, JORDAN6:55; :: thesis: verum

end;

LE p1,q1,P,p1,p2 by A7, A15, JORDAN5C:10;
hence A is_an_arc_of p1,q1 by A4, A7, JORDAN16:21; :: thesis: ( A c= C & A misses {p2,q2} )
A19: A c= P by JORDAN16:2;
hence A c= C by A11; :: thesis: A misses {p2,q2}
not q2 in A by A16, A19;
hence A misses {p2,q2} by A17, ZFMISC_1:51; :: thesis: verum

end;

hence p1,q1 are_neighbours_wrt p2,q2,C ; :: thesis: verum

end;

suppose that A20: q2 in P and
A21: not q1 in P ; :: thesis: p1,q1 are_neighbours_wrt p2,q2,C

now :: thesis: ex A being Element of bool the carrier of (TOP-REAL 2) st
( A is_an_arc_of p1,q1 & A c= C & A misses {p2,q2} )

take A = Segment (P1,p1,p2,p1,q1); :: thesis: ( A is_an_arc_of p1,q1 & A c= C & A misses {p2,q2} )

A22: now :: thesis: not p2 in A

A23: A = { q where q is Point of (TOP-REAL 2) : ( LE p1,q,P1,p1,p2 & LE q,q1,P1,p1,p2 ) } by JORDAN6:26;
assume p2 in A ; :: thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( p2 = q & LE p1,q,P1,p1,p2 & LE q,q1,P1,p1,p2 ) by A23;
hence contradiction by A5, A8, JORDAN6:55; :: thesis: verum

end;

q1 in P1 by A2, A9, A21, XBOOLE_0:def 3;
then LE p1,q1,P1,p1,p2 by A8, JORDAN5C:10;
hence A is_an_arc_of p1,q1 by A4, A8, JORDAN16:21; :: thesis: ( A c= C & A misses {p2,q2} )
A24: A c= P1 by JORDAN16:2;
hence A c= C by A14; :: thesis: A misses {p2,q2}

now :: thesis: not q2 in A

assume q2 in A ; :: thesis: contradiction
then q2 in {p1,p2} by A10, A20, A24, XBOOLE_0:def 4;
hence contradiction by A6, TARSKI:def 2; :: thesis: verum

end;

hence A misses {p2,q2} by A22, ZFMISC_1:51; :: thesis: verum

end;

hence p1,q1 are_neighbours_wrt p2,q2,C ; :: thesis: verum

end;

suppose A25: ( q1 in P & q2 in P ) ; :: thesis: p1,q1 are_neighbours_wrt p2,q2,C

P1 meets {q1,q2} by A12, A8, A9, XBOOLE_1:7;
then ( q1 in P1 or q2 in P1 ) by ZFMISC_1:51;
then ( q1 in {p1,p2} or q2 in {p1,p2} ) by A10, A25, XBOOLE_0:def 4;
hence p1,q1 are_neighbours_wrt p2,q2,C by A4, A5, A6, TARSKI:def 2; :: thesis: verum

end;

end;