let C be Simple_closed_curve; :: thesis: 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); :: thesis: 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); :: thesis: ( 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
; :: thesis: ( Upper_Arc C c= P or Lower_Arc C c= P )
A5:
W-min C <> E-max C
by TOPREAL5:25;
reconsider P' = P as non empty Subset of (TOP-REAL 2) by A3;
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
;
:: thesis: ( Upper_Arc C c= P or Lower_Arc C c= P )set S =
Segment P',
p1,
p2,
(W-min C),
(E-max C);
reconsider S' =
Segment P',
p1,
p2,
(W-min C),
(E-max C) as non
empty Subset of
(TOP-REAL 2) by A2, A6, Th9;
Segment P',
p1,
p2,
(W-min C),
(E-max C) c= P
by Th5;
then
Segment P',
p1,
p2,
(W-min C),
(E-max C) c= C
by A1, XBOOLE_1:1;
then
(
S' = Lower_Arc C or
S' = Upper_Arc C )
by A2, A5, A6, Th19, Th36;
hence
(
Upper_Arc C c= P or
Lower_Arc C c= P )
by Th5;
:: thesis: verum end; suppose A7:
LE E-max C,
W-min C,
P,
p1,
p2
;
:: thesis: ( Upper_Arc C c= P or Lower_Arc C c= P )set S =
Segment P',
p1,
p2,
(E-max C),
(W-min C);
reconsider S' =
Segment P',
p1,
p2,
(E-max C),
(W-min C) as non
empty Subset of
(TOP-REAL 2) by A2, A7, Th9;
A8:
Segment P',
p1,
p2,
(E-max C),
(W-min C) c= P
by Th5;
Segment P',
p1,
p2,
(E-max C),
(W-min C) is_an_arc_of E-max C,
W-min C
by A2, A5, A7, Th36;
then
S' is_an_arc_of W-min C,
E-max C
by JORDAN5B:14;
hence
(
Upper_Arc C c= P or
Lower_Arc C c= P )
by A1, A8, Th19, XBOOLE_1:1;
:: thesis: verum end;