let C be Simple_closed_curve; :: thesis:
let p be Point of (TOP-REAL 2); :: thesis:
set q = W-min C;
assume A1: LE p, E-max C,C ; :: thesis:
A2: p in Upper_Arc C by A1, JORDAN17:3;
A3: W-min C in Lower_Arc C by JORDAN7:1;
A4: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:65;
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] );
A5: for p1 being Point of (TOP-REAL 2) holds
( S₁[p1] iff S₄[p1] )

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:

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

A7: now

assume ( p1 in Lower_Arc C & p1 in Upper_Arc C ) ; :: thesis:
then p1 in (Lower_Arc C) /\ (Upper_Arc C) by 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 A7;

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 A3, 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 A3, A4, 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 A6, JORDAN6:def 10; :: thesis:

end;

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

A10: p1 in C by A6, A9, JORDAN7:5;
C = (Lower_Arc C) \/ (Upper_Arc C) by JORDAN6:def 9;
then p1 in Lower_Arc C by A8, A10, 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 A4, JORDAN5C:10; :: thesis:

end;

assume A11: ( 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:
A12: Upper_Arc C c= C by JORDAN6:76;

per cases by A11;

suppose A13: 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 A2, A13, JORDAN6:def 10; :: thesis:

end;

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

A15: p1 in Lower_Arc C by A14, JORDAN5C:def 3;

per cases ;

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

hence S₁[p1] by A2, A12; :: thesis:

end;

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

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

end;

hence S₁[p1] ; :: thesis:

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 Y' = { 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(A5);
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: