let C be Simple_closed_curve; :: thesis: 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); :: thesis: ( 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
; :: thesis: 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 that A5:
q1 <> p1
and A6:
q2 <> p2
and A7:
q1 <> p2
and A8:
q2 <> p1
;
:: thesis: q1,q2,C -separate p1,p2let A be
Subset of
(TOP-REAL 2);
:: according to JORDAN18:def 3 :: thesis: ( A is_an_arc_of q1,q2 & A c= C implies A meets {p1,p2} )assume that A9:
A is_an_arc_of q1,
q2
and A10:
A c= C
;
:: thesis: A meets {p1,p2}consider B being non
empty Subset of
(TOP-REAL 2) such that A11:
B is_an_arc_of q1,
q2
and A12:
A \/ B = C
and
A /\ B = {q1,q2}
by A9, A10, Th18;
assume
A misses {p1,p2}
;
:: thesis: contradictionthen
( not
p1 in A & not
p2 in A )
by ZFMISC_1:55;
then
(
p1 in B &
p2 in B )
by A2, A3, A12, XBOOLE_0:def 3;
then consider P being non
empty Subset of
(TOP-REAL 2) such that A13:
P is_an_arc_of p1,
p2
and A14:
P c= B
and A15:
P misses {q1,q2}
by A1, A5, A6, A7, A8, A11, JORDAN16:38;
B c= C
by A12, XBOOLE_1:7;
then
P c= C
by A14, XBOOLE_1:1;
hence
contradiction
by A4, A13, A15, Def3;
:: thesis: verum end;