let a, b, c, d be Point of (); :: thesis: for P being Subset of () st a <> b & P is_an_arc_of c,d & LE a,b,P,c,d holds
ex e being Point of () st
( a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d )

let P be Subset of (); :: thesis: ( a <> b & P is_an_arc_of c,d & LE a,b,P,c,d implies ex e being Point of () 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 () st
( a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d )

b in P by ;
then consider f being Function of I[01],(() | 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 ;
A9: rng f = [#] (() | P) by
.= the carrier of (() | P)
.= P by PRE_TOPC:8 ;
a in P by ;
then consider ra being object such that
A10: ra in dom f and
A11: a = f . ra by ;
A12: dom f = [#] I[01] by
.= [.0,1.] by BORSUK_1:40 ;
then reconsider ra = ra as Real by A10;
A13: 0 <= ra by ;
A14: ra <= 1 by ;
then ra <= rb by A3, A4, A5, A6, A7, A8, A11, A13, JORDAN5C:def 3;
then ra < rb by ;
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 ;
A18: 0 <= re by ;
then A19: re in dom f by ;
then f . re in rng f by FUNCT_1:def 3;
then reconsider e = f . re as Point of () 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 ;
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