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

{ p where p is Point of (TOP-REAL 2) : ( LE W-min P,p,P & LE p, E-max P,P ) } = Upper_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

A12:
E-max P <> W-min P
by A1, TOPREAL5:19;
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

end;proof

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 ) ) }
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 ) ) ;

end;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;

end;

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

end;

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;

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;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

proof

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
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;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

{ 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

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
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

end;proof

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 ) }
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 ;

end;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;

end;

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

end;

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

end;

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;then p = E-max P by A16, JORDAN6:54;

hence x in Upper_Arc P by A2, A14, TOPREAL1:1; :: thesis: verum

proof

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
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;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