let a, b, c, d be Point of (TOP-REAL 2); 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); ( 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
; 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
; ( a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d )
now ( not a = e & not b = e )assume A20:
(
a = e or
b = e )
;
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;
verum end;
hence
( 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; verum