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
and
A2:
p2 in C
and
A3:
q1 in C
and
A4:
p1 <> p2
and
A5:
q1 <> p1
and
A6:
q1 <> p2
and
A7:
q2 <> p1
and
A8:
q2 <> p2
; :: thesis: ( p1,p2 are_neighbours_wrt q1,q2,C or p1,q1 are_neighbours_wrt p2,q2,C )
assume A9:
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
consider P, P1 being non empty Subset of (TOP-REAL 2) such that
A10:
P is_an_arc_of p1,p2
and
A11:
P1 is_an_arc_of p1,p2
and
A12:
C = P \/ P1
and
A13:
P /\ P1 = {p1,p2}
by A1, A2, A4, TOPREAL2:5;
A14:
P c= C
by A12, XBOOLE_1:7;
A15:
P1 c= C
by A12, XBOOLE_1:7;
A16:
P meets {q1,q2}
by A9, A10, A12, 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 A16, ZFMISC_1:57;
suppose that A17:
q1 in P
and A18:
not
q2 in P
;
:: thesis: p1,q1 are_neighbours_wrt p2,q2,Cnow take A =
Segment P,
p1,
p2,
p1,
q1;
:: thesis: ( A is_an_arc_of p1,q1 & A c= C & A misses {p2,q2} )
LE p1,
q1,
P,
p1,
p2
by A10, A17, JORDAN5C:10;
hence
A is_an_arc_of p1,
q1
by A5, A10, JORDAN16:36;
:: thesis: ( A c= C & A misses {p2,q2} )A19:
A c= P
by JORDAN16:5;
hence
A c= C
by A14, XBOOLE_1:1;
:: thesis: A misses {p2,q2}A20:
now assume A21:
p2 in A
;
:: thesis: contradiction
A = { q where q is Point of (TOP-REAL 2) : ( LE p1,q,P,p1,p2 & LE q,q1,P,p1,p2 ) }
by JORDAN6:29;
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 A21;
hence
contradiction
by A6, A10, JORDAN6:70;
:: thesis: verum end;
not
q2 in A
by A18, A19;
hence
A misses {p2,q2}
by A20, ZFMISC_1:57;
:: thesis: verum end; hence
p1,
q1 are_neighbours_wrt p2,
q2,
C
by Def3;
:: thesis: verum suppose that A22:
q2 in P
and A23:
not
q1 in P
;
:: thesis: p1,q1 are_neighbours_wrt p2,q2,Cnow take A =
Segment P1,
p1,
p2,
p1,
q1;
:: thesis: ( A is_an_arc_of p1,q1 & A c= C & A misses {p2,q2} )
q1 in P1
by A3, A12, A23, XBOOLE_0:def 3;
then
LE p1,
q1,
P1,
p1,
p2
by A11, JORDAN5C:10;
hence
A is_an_arc_of p1,
q1
by A5, A11, JORDAN16:36;
:: thesis: ( A c= C & A misses {p2,q2} )A24:
A c= P1
by JORDAN16:5;
hence
A c= C
by A15, XBOOLE_1:1;
:: thesis: A misses {p2,q2}A25:
now assume A26:
p2 in A
;
:: thesis: contradiction
A = { q where q is Point of (TOP-REAL 2) : ( LE p1,q,P1,p1,p2 & LE q,q1,P1,p1,p2 ) }
by JORDAN6:29;
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 A26;
hence
contradiction
by A6, A11, JORDAN6:70;
:: thesis: verum end; hence
A misses {p2,q2}
by A25, ZFMISC_1:57;
:: thesis: verum end; hence
p1,
q1 are_neighbours_wrt p2,
q2,
C
by Def3;
:: thesis: verum suppose that A27:
q1 in P
and A28:
q2 in P
;
:: thesis: p1,q1 are_neighbours_wrt p2,q2,C
P1 meets {q1,q2}
by A9, A11, A12, XBOOLE_1:7;
then
(
q1 in P1 or
q2 in P1 )
by ZFMISC_1:57;
then
(
q1 in {p1,p2} or
q2 in {p1,p2} )
by A13, A27, A28, XBOOLE_0:def 4;
hence
p1,
q1 are_neighbours_wrt p2,
q2,
C
by A5, A6, A7, A8, TARSKI:def 2;
:: thesis: verum end;