let C be Simple_closed_curve; :: thesis: for p1, p2, q1, q2 being Point of () 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 (); :: 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 () 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 ;
A11: P c= C by ;
assume A12: for A being Subset of () 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 ;
A14: P1 c= C by ;
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 ;
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 () 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 () : ( 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 () 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 ;
hence A is_an_arc_of p1,q1 by ; :: 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 ;
hence A misses {p2,q2} by ; :: 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 () 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 () : ( 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 () 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 ;
then LE p1,q1,P1,p1,p2 by ;
hence A is_an_arc_of p1,q1 by ; :: 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 ;
hence contradiction by A6, TARSKI:def 2; :: thesis: verum
end;
hence A misses {p2,q2} by ; :: 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 ;
then ( q1 in P1 or q2 in P1 ) by ZFMISC_1:51;
then ( q1 in {p1,p2} or q2 in {p1,p2} ) by ;
hence p1,q1 are_neighbours_wrt p2,q2,C by ; :: thesis: verum
end;
end;