let p1, p2 be Point of (TOP-REAL 2); for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p2 in Upper_Arc P & LE p1,p2,P holds
p1 in Upper_Arc P
let P be non empty compact Subset of (TOP-REAL 2); ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p2 in Upper_Arc P & LE p1,p2,P implies p1 in Upper_Arc P )
assume that
A1:
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 }
and
A2:
p2 in Upper_Arc P
and
A3:
LE p1,p2,P
; p1 in Upper_Arc P
set P4b = Lower_Arc P;
A4:
( ( p1 in Upper_Arc P & p2 in Lower_Arc P & not p2 = W-min P ) or ( p1 in Upper_Arc P & p2 in Upper_Arc P & LE p1,p2, Upper_Arc P, W-min P, E-max P ) or ( p1 in Lower_Arc P & p2 in Lower_Arc P & not p2 = W-min P & LE p1,p2, Lower_Arc P, E-max P, W-min P ) )
by A3;
A5:
P is being_simple_closed_curve
by A1, JGRAPH_3:26;
then A6:
Lower_Arc P is_an_arc_of E-max P, W-min P
by JORDAN6:def 9;
A7:
(Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)}
by A5, JORDAN6:def 9;
then
E-max P in (Upper_Arc P) /\ (Lower_Arc P)
by TARSKI:def 2;
then A8:
E-max P in Upper_Arc P
by XBOOLE_0:def 4;
now p1 in Upper_Arc Passume A9:
not
p1 in Upper_Arc P
;
contradictionthen
p2 in (Upper_Arc P) /\ (Lower_Arc P)
by A2, A4, XBOOLE_0:def 4;
then A10:
p2 = E-max P
by A7, A4, A9, TARSKI:def 2;
then
LE p2,
p1,
Lower_Arc P,
E-max P,
W-min P
by A6, A4, A9, JORDAN5C:10;
hence
contradiction
by A6, A8, A4, A9, A10, JORDAN5C:12;
verum end;
hence
p1 in Upper_Arc P
; verum