let C be Simple_closed_curve; :: thesis: for P being connected compact Subset of (TOP-REAL 2) st P c= C & 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 connected compact Subset of (TOP-REAL 2); :: thesis: ( P c= C & 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: W-min C in P and
A3: E-max C in P ; :: thesis: ( Upper_Arc C c= P or Lower_Arc C c= P )
A4: now :: thesis: for p being Point of (TOP-REAL 2) holds not P = {p}
given p being Point of (TOP-REAL 2) such that A5: P = {p} ; :: thesis: contradiction
( W-min C = p & E-max C = p ) by A2, A3, A5, TARSKI:def 1;
hence contradiction by TOPREAL5:19; :: thesis: verum
end;
per cases ( ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 or P = C ) by A1, A2, A4, BORSUK_4:56;
suppose ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 ; :: thesis: ( Upper_Arc C c= P or Lower_Arc C c= P )
hence ( Upper_Arc C c= P or Lower_Arc C c= P ) by A1, A2, A3, JORDAN16:22; :: thesis: verum
end;
suppose P = C ; :: thesis: ( Upper_Arc C c= P or Lower_Arc C c= P )
hence ( Upper_Arc C c= P or Lower_Arc C c= P ) by JORDAN6:61; :: thesis: verum
end;
end;