let C be Simple_closed_curve; for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in C & p2 in C & p1,p2,C -separate q1,q2 holds
q1,q2,C -separate p1,p2
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ( p1 <> p2 & p1 in C & p2 in C & p1,p2,C -separate q1,q2 implies q1,q2,C -separate p1,p2 )
assume that
A1:
p1 <> p2
and
A2:
p1 in C
and
A3:
p2 in C
and
A4:
p1,p2,C -separate q1,q2
; q1,q2,C -separate p1,p2
per cases
( q1 = p1 or q2 = p2 or q1 = p2 or p1 = q2 or ( q1 <> p1 & q2 <> p2 & q1 <> p2 & q2 <> p1 ) )
;
suppose A5:
(
q1 <> p1 &
q2 <> p2 &
q1 <> p2 &
q2 <> p1 )
;
q1,q2,C -separate p1,p2let A be
Subset of
(TOP-REAL 2);
JORDAN18:def 3 ( A is_an_arc_of q1,q2 & A c= C implies A meets {p1,p2} )assume
(
A is_an_arc_of q1,
q2 &
A c= C )
;
A meets {p1,p2}then consider B being non
empty Subset of
(TOP-REAL 2) such that A6:
B is_an_arc_of q1,
q2
and A7:
A \/ B = C
and
A /\ B = {q1,q2}
by Th15;
assume A8:
A misses {p1,p2}
;
contradictionthen
not
p2 in A
by ZFMISC_1:49;
then A9:
p2 in B
by A3, A7, XBOOLE_0:def 3;
not
p1 in A
by A8, ZFMISC_1:49;
then
p1 in B
by A2, A7, XBOOLE_0:def 3;
then consider P being non
empty Subset of
(TOP-REAL 2) such that A10:
P is_an_arc_of p1,
p2
and A11:
P c= B
and A12:
P misses {q1,q2}
by A1, A5, A6, A9, JORDAN16:23;
B c= C
by A7, XBOOLE_1:7;
then
P c= C
by A11;
hence
contradiction
by A4, A10, A12;
verum end;