let C be Simple_closed_curve; for p1, p2 being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st P c= C & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P & not Upper_Arc C c= P holds
Lower_Arc C c= P
let p1, p2 be Point of (TOP-REAL 2); for P being Subset of (TOP-REAL 2) st P c= C & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P & not Upper_Arc C c= P holds
Lower_Arc C c= P
let P be Subset of (TOP-REAL 2); ( P c= C & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P & not Upper_Arc C c= P implies Lower_Arc C c= P )
assume that
A1:
P c= C
and
A2:
P is_an_arc_of p1,p2
and
A3:
W-min C in P
and
A4:
E-max C in P
; ( Upper_Arc C c= P or Lower_Arc C c= P )
reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A3;
A5:
W-min C <> E-max C
by TOPREAL5:19;
per cases
( LE W-min C, E-max C,P,p1,p2 or LE E-max C, W-min C,P,p1,p2 )
by A2, A3, A4, A5, JORDAN5C:14;
suppose A6:
LE W-min C,
E-max C,
P,
p1,
p2
;
( Upper_Arc C c= P or Lower_Arc C c= P )set S =
Segment (
P9,
p1,
p2,
(W-min C),
(E-max C));
reconsider S9 =
Segment (
P9,
p1,
p2,
(W-min C),
(E-max C)) as non
empty Subset of
(TOP-REAL 2) by A6, Th5;
Segment (
P9,
p1,
p2,
(W-min C),
(E-max C))
c= P
by Th2;
then
Segment (
P9,
p1,
p2,
(W-min C),
(E-max C))
c= C
by A1;
then
(
S9 = Lower_Arc C or
S9 = Upper_Arc C )
by A2, A5, A6, Th15, Th21;
hence
(
Upper_Arc C c= P or
Lower_Arc C c= P )
by Th2;
verum end; suppose A7:
LE E-max C,
W-min C,
P,
p1,
p2
;
( Upper_Arc C c= P or Lower_Arc C c= P )set S =
Segment (
P9,
p1,
p2,
(E-max C),
(W-min C));
reconsider S9 =
Segment (
P9,
p1,
p2,
(E-max C),
(W-min C)) as non
empty Subset of
(TOP-REAL 2) by A7, Th5;
Segment (
P9,
p1,
p2,
(E-max C),
(W-min C))
is_an_arc_of E-max C,
W-min C
by A2, A5, A7, Th21;
then A8:
S9 is_an_arc_of W-min C,
E-max C
by JORDAN5B:14;
Segment (
P9,
p1,
p2,
(E-max C),
(W-min C))
c= P
by Th2;
hence
(
Upper_Arc C c= P or
Lower_Arc C c= P )
by A1, A8, Th15, XBOOLE_1:1;
verum end;