let P be non empty compact Subset of (); :: thesis: ( P is being_simple_closed_curve implies ( Segment ((),(),P) = Upper_Arc P & Segment ((),(),P) = Lower_Arc P ) )
assume A1: P is being_simple_closed_curve ; :: thesis: ( Segment ((),(),P) = Upper_Arc P & Segment ((),(),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 () : ( 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 () : ( 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 () : ( 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 () : ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) } ; :: thesis:
then consider p1 being Point of () 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;
end;
Lower_Arc P c= { p1 where p1 is Point of () : ( 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 () : ( 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 () : ( LE E-max P,p1,P or ( E-max P in P & p1 = W-min P ) ) }
then reconsider p2 = x as Point of () ;
Upper_Arc P is_an_arc_of W-min P, E-max P by ;
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 ;
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 () : ( 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 () : ( 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 ;
{ p where p is Point of () : ( LE W-min P,p,P & LE p, E-max P,P ) } = Upper_Arc P
proof
A13: { p where p is Point of () : ( 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 () : ( 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 () : ( LE W-min P,p,P & LE p, E-max P,P ) } ; :: thesis:
then consider p being Point of () 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 ;
end;
end;
Upper_Arc P c= { p where p is Point of () : ( 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 () : ( 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 () : ( LE W-min P,p,P & LE p, E-max P,P ) }
then reconsider p2 = x as Point of () ;
E-max P in Lower_Arc P by ;
then A18: LE p2, E-max P,P by ;
A19: W-min P in Upper_Arc P by ;
LE W-min P,p2, Upper_Arc P, W-min P, E-max P by ;
then LE W-min P,p2,P by ;
hence x in { p where p is Point of () : ( LE W-min P,p,P & LE p, E-max P,P ) } by A18; :: thesis: verum
end;
hence { p where p is Point of () : ( LE W-min P,p,P & LE p, E-max P,P ) } = Upper_Arc P by A13; :: thesis: verum
end;
hence ( Segment ((),(),P) = Upper_Arc P & Segment ((),(),P) = Lower_Arc P ) by ; :: thesis: verum