let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & q1 <> q2 holds
ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} )
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & q1 <> q2 implies ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} ) )
assume that
A1: P is_an_arc_of p1,p2 and
A2: ( q1 in P & q2 in P ) and
A3: q1 <> p1 and
A4: q1 <> p2 and
A5: q2 <> p1 and
A6: q2 <> p2 and
A7: q1 <> q2 ; :: thesis: ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} )
per cases ( LE q1,q2,P,p1,p2 or LE q2,q1,P,p1,p2 ) by A1, A2, A7, JORDAN5C:14;
suppose A8: LE q1,q2,P,p1,p2 ; :: thesis: ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} )
set S = Segment (P,p1,p2,q1,q2);
Segment (P,p1,p2,q1,q2) is_an_arc_of q1,q2 by A1, A7, A8, Th21;
then reconsider S = Segment (P,p1,p2,q1,q2) as non empty Subset of (TOP-REAL 2) by TOPREAL1:1;
take S ; :: thesis: ( S is_an_arc_of q1,q2 & S c= P & S misses {p1,p2} )
thus S is_an_arc_of q1,q2 by A1, A7, A8, Th21; :: thesis: ( S c= P & S misses {p1,p2} )
thus S c= P by Th2; :: thesis: S misses {p1,p2}
now :: thesis: not S meets {p1,p2}
A9: S = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } by JORDAN6:26;
assume A10: S meets {p1,p2} ; :: thesis: contradiction
per cases ( p1 in S or p2 in S ) by A10, ZFMISC_1:51;
suppose p1 in S ; :: thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( q = p1 & LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) by A9;
hence contradiction by A1, A3, JORDAN6:54; :: thesis: verum
end;
suppose p2 in S ; :: thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( q = p2 & LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) by A9;
hence contradiction by A1, A6, JORDAN6:55; :: thesis: verum
end;
end;
end;
hence S misses {p1,p2} ; :: thesis: verum
end;
suppose A11: LE q2,q1,P,p1,p2 ; :: thesis: ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} )
set S = Segment (P,p1,p2,q2,q1);
Segment (P,p1,p2,q2,q1) is_an_arc_of q2,q1 by A1, A7, A11, Th21;
then reconsider S = Segment (P,p1,p2,q2,q1) as non empty Subset of (TOP-REAL 2) by TOPREAL1:1;
take S ; :: thesis: ( S is_an_arc_of q1,q2 & S c= P & S misses {p1,p2} )
S is_an_arc_of q2,q1 by A1, A7, A11, Th21;
hence S is_an_arc_of q1,q2 by JORDAN5B:14; :: thesis: ( S c= P & S misses {p1,p2} )
thus S c= P by Th2; :: thesis: S misses {p1,p2}
now :: thesis: not S meets {p1,p2}
A12: S = { q where q is Point of (TOP-REAL 2) : ( LE q2,q,P,p1,p2 & LE q,q1,P,p1,p2 ) } by JORDAN6:26;
assume A13: S meets {p1,p2} ; :: thesis: contradiction
per cases ( p1 in S or p2 in S ) by A13, ZFMISC_1:51;
suppose p1 in S ; :: thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( q = p1 & LE q2,q,P,p1,p2 & LE q,q1,P,p1,p2 ) by A12;
hence contradiction by A1, A5, JORDAN6:54; :: thesis: verum
end;
suppose p2 in S ; :: thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( q = p2 & LE q2,q,P,p1,p2 & LE q,q1,P,p1,p2 ) by A12;
hence contradiction by A1, A4, JORDAN6:55; :: thesis: verum
end;
end;
end;
hence S misses {p1,p2} ; :: thesis: verum
end;
end;