let C be Simple_closed_curve; :: thesis:
let p be Point of (TOP-REAL 2); :: thesis:
set q = W-min C;
assume LE p, E-max C,C ; :: thesis:
then A1: p in Upper_Arc C by JORDAN17:3;
A2: W-min C in Lower_Arc C by JORDAN7:1;
A3: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
defpred S₁[ Point of (TOP-REAL 2)] means ( LE p,$1,C or ( p in C & $1 = W-min C ) );
defpred S₂[ Point of (TOP-REAL 2)] means LE p,$1, Upper_Arc C, W-min C, E-max C;
defpred S₃[ Point of (TOP-REAL 2)] means LE $1, W-min C, Lower_Arc C, E-max C, W-min C;
defpred S₄[ Point of (TOP-REAL 2)] means ( S₂[$1] or S₃[$1] );
A4: for p1 being Point of (TOP-REAL 2) holds
( S₁[p1] iff S₄[p1] )

proof

let p1 be Point of (TOP-REAL 2); :: thesis:
thus ( ( not LE p,p1,C & not ( p in C & p1 = W-min C ) ) or LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) :: thesis:

proof

assume A5: ( LE p,p1,C or ( p in C & p1 = W-min C ) ) ; :: thesis:

A6: now :: thesis:

assume that
A7: p1 in Lower_Arc C and
A8: p1 in Upper_Arc C ; :: thesis:
p1 in (Lower_Arc C) /\ (Upper_Arc C) by A7, A8, XBOOLE_0:def 4;
then p1 in {(W-min C),(E-max C)} by JORDAN6:def 9;
hence ( p1 = W-min C or p1 = E-max C ) by TARSKI:def 2; :: thesis:

end;

per cases by A6;

suppose p1 = W-min C ; :: thesis:

hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A2, JORDAN5C:9; :: thesis:

end;

suppose p1 = E-max C ; :: thesis:

hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A2, A3, JORDAN5C:10; :: thesis:

end;

suppose ( not p1 in Lower_Arc C & p1 <> W-min C ) ; :: thesis:

hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A5, JORDAN6:def 10; :: thesis:

end;

suppose that A9: not p1 in Upper_Arc C and
A10: p1 <> W-min C ; :: thesis:

A11: p1 in C by A5, A10, JORDAN7:5;
C = (Lower_Arc C) \/ (Upper_Arc C) by JORDAN6:def 9;
then p1 in Lower_Arc C by A9, A11, XBOOLE_0:def 3;
hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A3, JORDAN5C:10; :: thesis:

end;

end;

end;

assume A12: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) ; :: thesis:
A13: Upper_Arc C c= C by JORDAN6:61;

per cases by A12;

suppose A14: LE p,p1, Upper_Arc C, W-min C, E-max C ; :: thesis:

then p1 in Upper_Arc C by JORDAN5C:def 3;
hence S₁[p1] by A1, A14, JORDAN6:def 10; :: thesis:

end;

suppose LE p1, W-min C, Lower_Arc C, E-max C, W-min C ; :: thesis:

then A15: p1 in Lower_Arc C by JORDAN5C:def 3;

now :: thesis:

per cases ;

suppose p1 = W-min C ; :: thesis:

hence S₁[p1] by A1, A13; :: thesis:

end;

suppose p1 <> W-min C ; :: thesis:

hence S₁[p1] by A1, A15, JORDAN6:def 10; :: thesis:

end;

end;

end;

hence S₁[p1] ; :: thesis:

end;

end;

end;

set Y1 = { p1 where p1 is Point of (TOP-REAL 2) : S₂[p1] } ;
set Y2 = { p1 where p1 is Point of (TOP-REAL 2) : S₃[p1] } ;
deffunc H₁( set ) -> set = $1;
set X = { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₁[p1] } ;
set Y = { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₄[p1] } ;
set Y9 = { p1 where p1 is Point of (TOP-REAL 2) : ( S₂[p1] or S₃[p1] ) } ;
A16: { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₁[p1] } = { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₄[p1] } from FRAENKEL:sch 3(A4);
A17: Segment (p,(W-min C),C) = { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₁[p1] } by JORDAN7:def 1;
A18: L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) = { p1 where p1 is Point of (TOP-REAL 2) : S₃[p1] } by JORDAN6:def 3;
{ p1 where p1 is Point of (TOP-REAL 2) : ( S₂[p1] or S₃[p1] ) } = { p1 where p1 is Point of (TOP-REAL 2) : S₂[p1] } \/ { p1 where p1 is Point of (TOP-REAL 2) : S₃[p1] } from TOPREAL1:sch 1();
hence Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) by A16, A17, A18, JORDAN6:def 4; :: thesis: