let C be Simple_closed_curve; :: thesis:
let p, q be Point of (TOP-REAL 2); :: thesis:
assume that
A1: LE p, E-max C,C and
A2: LE E-max C,q,C ; :: thesis:
A3: p in Upper_Arc C by A1, JORDAN17:3;
A4: q in Lower_Arc C by A2, JORDAN17:4;

A5: now :: thesis:

assume q = W-min C ; :: thesis:
then W-min C = E-max C by A2, JORDAN7:2;
hence contradiction by TOPREAL5:19; :: thesis:

end;

A6: 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 & LE $1,q,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,q, Lower_Arc C, E-max C, W-min C;
defpred S₄[ Point of (TOP-REAL 2)] means ( S₂[$1] or S₃[$1] );
A7: 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 ( LE p,p1,C & LE p1,q,C & not LE p,p1, Upper_Arc C, W-min C, E-max C implies LE p1,q, Lower_Arc C, E-max C, W-min C ) :: thesis:

proof

assume that
A8: LE p,p1,C and
A9: LE p1,q,C ; :: thesis:

A10: now :: thesis:

assume that
A11: p1 in Lower_Arc C and
A12: p1 in Upper_Arc C ; :: thesis:
p1 in (Lower_Arc C) /\ (Upper_Arc C) by A11, A12, 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 A10;

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

then p = W-min C by A8, JORDAN7:2;
hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) by A1, A13, JORDAN17:3, 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,q, Lower_Arc C, E-max C, W-min C ) by A4, A6, JORDAN5C:10; :: thesis:

end;

suppose not p1 in Lower_Arc C ; :: thesis:

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

end;

suppose not p1 in Upper_Arc C ; :: thesis:

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

end;

end;

end;

assume A14: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) ; :: thesis:

per cases by A14;

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

then A16: p1 in Upper_Arc C by JORDAN5C:def 3;
hence LE p,p1,C by A3, A15, JORDAN6:def 10; :: thesis:
thus LE p1,q,C by A4, A5, A16, JORDAN6:def 10; :: thesis:

end;

suppose that A17: LE p1,q, Lower_Arc C, E-max C, W-min C and
A18: p1 <> W-min C ; :: thesis:

A19: p1 in Lower_Arc C by A17, JORDAN5C:def 3;
hence LE p,p1,C by A3, A18, JORDAN6:def 10; :: thesis:
thus LE p1,q,C by A4, A5, A17, A19, JORDAN6:def 10; :: thesis:

end;

suppose ( LE p1,q, Lower_Arc C, E-max C, W-min C & p1 = W-min C ) ; :: thesis:

hence S₁[p1] by A5, A6, JORDAN6:55; :: 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] ) } ;
A20: { 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(A7);
A21: Segment (p,q,C) = { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₁[p1] } by A5, JORDAN7:def 1;
A22: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) = { 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,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) by A20, A21, A22, JORDAN6:def 4; :: thesis: