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 )

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

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 )

hence
( a <> e & b <> e )
; :: thesis: ( LE a,e,P,c,d & LE e,b,P,c,d )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;( 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

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