let a, b, c, d be Point of (TOP-REAL 2); :: thesis:
let P be Subset of (TOP-REAL 2); :: thesis:
assume that
A1: a <> b and
A2: P is_an_arc_of c,d and
A3: LE a,b,P,c,d ; :: thesis:
A4: a in P by A3, JORDAN5C:def 3;
b in P by A3, JORDAN5C:def 3;
then consider f being Function of I[01] ,((TOP-REAL 2) | P), rb being Real such that
A5: f is being_homeomorphism and
A6: f . 0 = c and
A7: f . 1 = d and
A8: 0 <= rb and
A9: rb <= 1 and
A10: f . rb = b by A2, Th1;
A11: rng f = [#] ((TOP-REAL 2) | P) by A5, TOPS_2:def 5
.= the carrier of ((TOP-REAL 2) | P)
.= P by PRE_TOPC:29 ;
then consider ra being set such that
A12: ra in dom f and
A13: a = f . ra by A4, FUNCT_1:def 5;
A14: dom f = [#] I[01] by A5, TOPS_2:def 5
.= [.0 ,1.] by BORSUK_1:83 ;
then reconsider ra = ra as Real by A12;
A15: 0 <= ra by A12, A14, XXREAL_1:1;
A16: ra <= 1 by A12, A14, XXREAL_1:1;
then ra <= rb by A3, A5, A6, A7, A8, A9, A10, A13, A15, JORDAN5C:def 3;
then ra < rb by A1, A10, A13, XXREAL_0:1;
then consider re being real number such that
A17: ra < re and
A18: re < rb by XREAL_1:7;
A19: re is Real by XREAL_0:def 1;
A20: ( 0 <= re & re <= 1 ) by A9, A15, A17, A18, XXREAL_0:2;
set e = f . re;
A21: re in dom f by A14, A20, XXREAL_1:1;
then f . re in rng f by FUNCT_1:def 5;
then reconsider e = f . re as Point of (TOP-REAL 2) by A11;
take e ; :: thesis:

now

assume A22: ( a = e or b = e ) ; :: thesis:
A23: f is one-to-one by A5, TOPS_2:def 5;
( ra in dom f & rb in dom f ) by A8, A9, A12, A14, XXREAL_1:1;
hence contradiction by A10, A13, A17, A18, A21, A22, A23, FUNCT_1:def 8; :: thesis:

end;

hence ( a <> e & b <> e ) ; :: thesis:
thus ( LE a,e,P,c,d & LE e,b,P,c,d ) by A2, A5, A6, A7, A8, A9, A10, A13, A15, A16, A17, A18, A19, A20, JORDAN5C:8; :: thesis: