let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve implies ( Segment ((W-min P),(E-max P),P) = Upper_Arc P & Segment ((E-max P),(W-min P),P) = Lower_Arc P ) )
assume A1: P is being_simple_closed_curve ; :: thesis: ( Segment ((W-min P),(E-max P),P) = Upper_Arc P & Segment ((E-max P),(W-min P),P) = Lower_Arc P )
then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by JORDAN6:def 8;
A3: { p1 where p1 is Point of (TOP-REAL 2) : ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) } = Lower_Arc P

proof

A4: { p1 where p1 is Point of (TOP-REAL 2) : ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) } c= Lower_Arc P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p1 where p1 is Point of (TOP-REAL 2) : ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) } or x in Lower_Arc P )
assume x in { p1 where p1 is Point of (TOP-REAL 2) : ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) } ; :: thesis: x in Lower_Arc P
then consider p1 being Point of (TOP-REAL 2) such that
A5: p1 = x and
A6: ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) ;

per cases ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) by A6;

suppose A7: LE E-max P,p1,P ; :: thesis: x in Lower_Arc P

per cases ( x in Lower_Arc P or ( E-max P in Upper_Arc P & p1 in Upper_Arc P & LE E-max P,p1, Upper_Arc P, W-min P, E-max P ) ) by A5, A7, JORDAN6:def 10;

suppose x in Lower_Arc P ; :: thesis: x in Lower_Arc P

hence x in Lower_Arc P ; :: thesis: verum

end;

suppose A8: ( E-max P in Upper_Arc P & p1 in Upper_Arc P & LE E-max P,p1, Upper_Arc P, W-min P, E-max P ) ; :: thesis: x in Lower_Arc P

A9: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, JORDAN6:50;
then LE p1, E-max P, Upper_Arc P, W-min P, E-max P by A8, JORDAN5C:10;
then A10: p1 = E-max P by A8, A9, JORDAN5C:12;
Lower_Arc P is_an_arc_of E-max P, W-min P by A1, JORDAN6:def 9;
hence x in Lower_Arc P by A5, A10, TOPREAL1:1; :: thesis: verum

end;

end;

end;

suppose ( E-max P in P & p1 = W-min P ) ; :: thesis: x in Lower_Arc P

then x in {(W-min P),(E-max P)} by A5, TARSKI:def 2;
then x in (Upper_Arc P) /\ (Lower_Arc P) by A1, JORDAN6:def 9;
hence x in Lower_Arc P by XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

Lower_Arc P c= { p1 where p1 is Point of (TOP-REAL 2) : ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lower_Arc P or x in { p1 where p1 is Point of (TOP-REAL 2) : ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) } )
assume A11: x in Lower_Arc P ; :: thesis: x in { p1 where p1 is Point of (TOP-REAL 2) : ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) }
then reconsider p2 = x as Point of (TOP-REAL 2) ;
Upper_Arc P is_an_arc_of W-min P, E-max P by A1, JORDAN6:50;
then ( ( not E-max P in P or not p2 = W-min P ) implies ( E-max P in Upper_Arc P & p2 in Lower_Arc P & not p2 = W-min P ) ) by A11, SPRECT_1:14, TOPREAL1:1;
then ( LE E-max P,p2,P or ( E-max P in P & p2 = W-min P ) ) by JORDAN6:def 10;
hence x in { p1 where p1 is Point of (TOP-REAL 2) : ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) } ; :: thesis: verum

end;

hence { p1 where p1 is Point of (TOP-REAL 2) : ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) } = Lower_Arc P by A4; :: thesis: verum

end;

A12: E-max P <> W-min P by A1, TOPREAL5:19;
{ p where p is Point of (TOP-REAL 2) : ( LE W-min P,p,P & LE p, E-max P,P ) } = Upper_Arc P

proof

A13: { p where p is Point of (TOP-REAL 2) : ( LE W-min P,p,P & LE p, E-max P,P ) } c= Upper_Arc P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : ( LE W-min P,p,P & LE p, E-max P,P ) } or x in Upper_Arc P )
assume x in { p where p is Point of (TOP-REAL 2) : ( LE W-min P,p,P & LE p, E-max P,P ) } ; :: thesis: x in Upper_Arc P
then consider p being Point of (TOP-REAL 2) such that
A14: p = x and
LE W-min P,p,P and
A15: LE p, E-max P,P ;

per cases ( ( p in Upper_Arc P & E-max P in Lower_Arc P & not E-max P = W-min P ) or ( p in Upper_Arc P & E-max P in Upper_Arc P & LE p, E-max P, Upper_Arc P, W-min P, E-max P ) or ( p in Lower_Arc P & E-max P in Lower_Arc P & not E-max P = W-min P & LE p, E-max P, Lower_Arc P, E-max P, W-min P ) ) by A15, JORDAN6:def 10;

suppose ( p in Upper_Arc P & E-max P in Lower_Arc P & not E-max P = W-min P ) ; :: thesis: x in Upper_Arc P

hence x in Upper_Arc P by A14; :: thesis: verum

end;

suppose ( p in Upper_Arc P & E-max P in Upper_Arc P & LE p, E-max P, Upper_Arc P, W-min P, E-max P ) ; :: thesis: x in Upper_Arc P

hence x in Upper_Arc P by A14; :: thesis: verum

end;

suppose A16: ( p in Lower_Arc P & E-max P in Lower_Arc P & not E-max P = W-min P & LE p, E-max P, Lower_Arc P, E-max P, W-min P ) ; :: thesis: x in Upper_Arc P

Lower_Arc P is_an_arc_of E-max P, W-min P by A1, JORDAN6:def 9;
then p = E-max P by A16, JORDAN6:54;
hence x in Upper_Arc P by A2, A14, TOPREAL1:1; :: thesis: verum

end;

end;

end;

Upper_Arc P c= { p where p is Point of (TOP-REAL 2) : ( LE W-min P,p,P & LE p, E-max P,P ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Upper_Arc P or x in { p where p is Point of (TOP-REAL 2) : ( LE W-min P,p,P & LE p, E-max P,P ) } )
assume A17: x in Upper_Arc P ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : ( LE W-min P,p,P & LE p, E-max P,P ) }
then reconsider p2 = x as Point of (TOP-REAL 2) ;
E-max P in Lower_Arc P by A1, Th1;
then A18: LE p2, E-max P,P by A12, A17, JORDAN6:def 10;
A19: W-min P in Upper_Arc P by A1, Th1;
LE W-min P,p2, Upper_Arc P, W-min P, E-max P by A2, A17, JORDAN5C:10;
then LE W-min P,p2,P by A17, A19, JORDAN6:def 10;
hence x in { p where p is Point of (TOP-REAL 2) : ( LE W-min P,p,P & LE p, E-max P,P ) } by A18; :: thesis: verum

end;

hence { p where p is Point of (TOP-REAL 2) : ( LE W-min P,p,P & LE p, E-max P,P ) } = Upper_Arc P by A13; :: thesis: verum

end;

hence ( Segment ((W-min P),(E-max P),P) = Upper_Arc P & Segment ((E-max P),(W-min P),P) = Lower_Arc P ) by A12, A3, Def1; :: thesis: verum