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;

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;

end;

suppose that A15:
q1 in P
and

A16: not q2 in P ; :: thesis: p1,q1 are_neighbours_wrt p2,q2,C

end;

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} )

hence
p1,q1 are_neighbours_wrt p2,q2,C
; :: thesis: verum( 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} )

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;A17: now :: thesis: not p2 in A

LE p1,q1,P,p1,p2
by A7, A15, JORDAN5C:10;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;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

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

suppose that A20:
q2 in P
and

A21: not q1 in P ; :: thesis: p1,q1 are_neighbours_wrt p2,q2,C

end;

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} )

hence
p1,q1 are_neighbours_wrt p2,q2,C
; :: thesis: verum( 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} )

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}

end;A22: now :: thesis: not p2 in A

q1 in P1
by A2, A9, A21, XBOOLE_0:def 3;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;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

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

hence
A misses {p2,q2}
by A22, ZFMISC_1:51; :: thesis: verumassume
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;then q2 in {p1,p2} by A10, A20, A24, XBOOLE_0:def 4;

hence contradiction by A6, TARSKI:def 2; :: thesis: verum

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;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