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: E-max P <> W-min P by TOPREAL5:25;
A3: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, JORDAN6:def 8;
A4: { 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

A5: { 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 set ; :: 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
A6: ( p = x & LE W-min P,p,P & 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 A6, 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 A6; :: 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 A6; :: thesis: verum

end;

suppose A7: ( 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 A7, JORDAN6:69;
hence x in Upper_Arc P by A3, A6, TOPREAL1:4; :: 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 set ; :: 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 A8: 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) ;
A9: ( W-min P in Lower_Arc P & E-max P in Lower_Arc P & W-min P in Upper_Arc P & E-max P in Upper_Arc P ) by A1, Th1;
LE W-min P,p2, Upper_Arc P, W-min P, E-max P by A3, A8, JORDAN5C:10;
then A10: LE W-min P,p2,P by A8, A9, JORDAN6:def 10;
LE p2, E-max P,P by A2, A8, A9, 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 A10; :: 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 A5, XBOOLE_0:def 10; :: thesis: verum

end;

{ 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

A11: { 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 set ; :: 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
A12: ( p1 = x & ( 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 A12;

suppose A13: 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 A12, A13, 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 A14: ( 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

A15: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, JORDAN6:65;
then LE p1, E-max P, Upper_Arc P, W-min P, E-max P by A14, JORDAN5C:10;
then A16: p1 = E-max P by A14, A15, 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 A12, A16, TOPREAL1:4; :: 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 A12, 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 set ; :: 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 A17: 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:65;
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 A17, SPRECT_1:16, TOPREAL1:4;
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 A11, XBOOLE_0:def 10; :: 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 A2, A4, Def1; :: thesis: verum