let P be Subset of (TOP-REAL 2); 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); ( 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
; 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
;
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
;
( 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;
( S c= P & S misses {p1,p2} )thus
S c= P
by Th2;
S misses {p1,p2}now 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}
;
contradictionper cases
( p1 in S or p2 in S )
by A10, ZFMISC_1:51;
suppose
p1 in S
;
contradictionthen
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;
verum end; suppose
p2 in S
;
contradictionthen
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;
verum end; end; end; hence
S misses {p1,p2}
;
verum end; suppose A11:
LE q2,
q1,
P,
p1,
p2
;
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
;
( 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;
( S c= P & S misses {p1,p2} )thus
S c= P
by Th2;
S misses {p1,p2}now 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}
;
contradictionper cases
( p1 in S or p2 in S )
by A13, ZFMISC_1:51;
suppose
p1 in S
;
contradictionthen
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;
verum end; suppose
p2 in S
;
contradictionthen
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;
verum end; end; end; hence
S misses {p1,p2}
;
verum end; end;