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

now :: thesis: ( not a = e & not b = e )

assume A20: ( a = e or b = e ) ; :: thesis: contradiction
( f is one-to-one & rb in dom f ) by A4, A6, A7, A12, TOPS_2:def 5, XXREAL_1:1;
hence contradiction by A8, A10, A11, A15, A16, A19, A20, FUNCT_1:def 4; :: thesis: verum

end;

hence ( a <> e & b <> e ) ; :: thesis: ( LE a,e,P,c,d & LE e,b,P,c,d )
thus ( LE a,e,P,c,d & LE e,b,P,c,d ) by A2, A4, A5, A6, A7, A8, A11, A13, A14, A15, A16, A18, A17, JORDAN5C:8; :: thesis: verum