let C be Simple_closed_curve; :: thesis: for p1, p2, q1, q2 being Point of () 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 (); :: 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 q1 = p1 ; :: thesis: q1,q2,C -separate p1,p2
hence q1,q2,C -separate p1,p2 by Th27; :: thesis: verum
end;
suppose q2 = p2 ; :: thesis: q1,q2,C -separate p1,p2
hence q1,q2,C -separate p1,p2 by Th28; :: thesis: verum
end;
suppose q1 = p2 ; :: thesis: q1,q2,C -separate p1,p2
hence q1,q2,C -separate p1,p2 by Th30; :: thesis: verum
end;
suppose p1 = q2 ; :: thesis: q1,q2,C -separate p1,p2
hence q1,q2,C -separate p1,p2 by Th29; :: thesis: verum
end;
suppose A5: ( q1 <> p1 & q2 <> p2 & q1 <> p2 & q2 <> p1 ) ; :: thesis: q1,q2,C -separate p1,p2
let A be Subset of (); :: according to JORDAN18:def 3 :: thesis: ( 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 ) ; :: thesis: A meets {p1,p2}
then consider B being non empty Subset of () 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} ; :: thesis: contradiction
then not p2 in A by ZFMISC_1:49;
then A9: p2 in B by ;
not p1 in A by ;
then p1 in B by ;
then consider P being non empty Subset of () such that
A10: P is_an_arc_of p1,p2 and
A11: P c= B and
A12: P misses {q1,q2} by ;
B c= C by ;
then P c= C by A11;
hence contradiction by A4, A10, A12; :: thesis: verum
end;
end;