let P be non empty compact Subset of (TOP-REAL 2); ( 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
; ( 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 ;
TARSKI:def 3 ( 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 ) ) }
;
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
;
x in Lower_Arc Pper 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 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 )
;
x in Lower_Arc PA9:
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;
verum 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 ;
TARSKI:def 3 ( 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
;
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 ) ) }
;
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;
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 ;
TARSKI:def 3 ( 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 ) }
;
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;
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 ;
TARSKI:def 3 ( 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
;
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;
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;
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; verum