let C be Simple_closed_curve; :: thesis:
let p, q be Point of (TOP-REAL 2); :: thesis:
assume that
A1: LE p,q,C and
A2: LE E-max C,p,C ; :: thesis:

per cases ;

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

hence Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) by A1, Th9; :: thesis:

end;

suppose A3: p <> E-max C ; :: thesis:

A4: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
A5: q in Lower_Arc C by A1, A2, JORDAN17:4, JORDAN6:58;
A6: p in Lower_Arc C by A2, JORDAN17:4;
A7: Lower_Arc C c= C by JORDAN6:61;

A8: now :: thesis:

assume A9: p = W-min C ; :: thesis:
then LE p, E-max C,C by JORDAN17:2;
hence contradiction by A2, A9, JORDAN6:57, TOPREAL5:19; :: thesis:

end;

A10: now :: thesis:

assume A11: q = W-min C ; :: thesis:
then LE q,p,C by A6, A7, JORDAN7:3;
hence contradiction by A1, A8, A11, JORDAN6:57; :: thesis:

end;

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, Lower_Arc C, E-max C, W-min C & LE $1,q, Lower_Arc C, E-max C, W-min C );
A12: for p1 being Point of (TOP-REAL 2) holds
( S₁[p1] iff S₂[p1] )

proof

let p1 be Point of (TOP-REAL 2); :: thesis:

hereby :: thesis:

assume that
A13: LE p,p1,C and
A14: LE p1,q,C ; :: thesis:

A15: now :: thesis:

assume A16: p1 = W-min C ; :: thesis:
then LE p1,p,C by A6, A7, JORDAN7:3;
hence contradiction by A8, A13, A16, JORDAN6:57; :: thesis:

end;

A17: now :: thesis:

assume A18: p in Upper_Arc C ; :: thesis:
p in Lower_Arc C by A2, JORDAN17:4;
then p in (Lower_Arc C) /\ (Upper_Arc C) by A18, XBOOLE_0:def 4;
then p in {(W-min C),(E-max C)} by JORDAN6:50;
hence contradiction by A3, A8, TARSKI:def 2; :: thesis:

end;

hence LE p,p1, Lower_Arc C, E-max C, W-min C by A13, JORDAN6:def 10; :: thesis:
A19: p1 in Lower_Arc C by A13, A17, JORDAN6:def 10;

per cases ;

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

hence LE p1,q, Lower_Arc C, E-max C, W-min C by A1, A2, A3, JORDAN6:57; :: thesis:

end;

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

hence LE p1,q, Lower_Arc C, E-max C, W-min C by A4, A5, JORDAN5C:10; :: thesis:

end;

suppose A20: p1 <> E-max C ; :: thesis:

now :: thesis:

assume p1 in Upper_Arc C ; :: thesis:
then p1 in (Lower_Arc C) /\ (Upper_Arc C) by A19, XBOOLE_0:def 4;
then p1 in {(W-min C),(E-max C)} by JORDAN6:50;
hence contradiction by A15, A20, TARSKI:def 2; :: thesis:

end;

hence LE p1,q, Lower_Arc C, E-max C, W-min C by A14, JORDAN6:def 10; :: thesis:

end;

end;

end;

assume that
A21: LE p,p1, Lower_Arc C, E-max C, W-min C and
A22: LE p1,q, Lower_Arc C, E-max C, W-min C ; :: thesis:
A23: p1 <> W-min C by A4, A10, A22, JORDAN6:55;
A24: p1 in Lower_Arc C by A21, JORDAN5C:def 3;
hence LE p,p1,C by A6, A21, A23, JORDAN6:def 10; :: thesis:
thus LE p1,q,C by A5, A10, A22, A24, JORDAN6:def 10; :: thesis:

end;

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] } ;
A25: { 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(A12);
Segment (p,q,C) = { H₁(p1) where p1 is Point of (TOP-REAL 2) : S₁[p1] } by A10, JORDAN7:def 1;
hence Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) by A25, JORDAN6:26; :: thesis:

end;

end;