let P be non empty Subset of (TOP-REAL 2); ( P is being_simple_closed_curve implies for r being Real ex p being Point of (TOP-REAL 2) st
( p in P & not p `2 = r ) )
assume A1:
P is being_simple_closed_curve
; for r being Real ex p being Point of (TOP-REAL 2) st
( p in P & not p `2 = r )
now for r0 being Real ex p being Point of (TOP-REAL 2) st
( p in P & not p `2 = r0 )A2:
[.0,1.] = ].0,1.[ \/ {0,1}
by XXREAL_1:128;
given r0 being
Real such that A3:
for
p being
Point of
(TOP-REAL 2) st
p in P holds
p `2 = r0
;
contradictionconsider p1,
p2 being
Point of
(TOP-REAL 2),
P1,
P2 being non
empty Subset of
(TOP-REAL 2) such that A4:
p1 <> p2
and A5:
p1 in P
and A6:
p2 in P
and A7:
P1 is_an_arc_of p1,
p2
and A8:
P2 is_an_arc_of p1,
p2
and A9:
P = P1 \/ P2
and A10:
P1 /\ P2 = {p1,p2}
by A1, TOPREAL2:6;
A11:
p1 `2 = r0
by A3, A5;
A12:
p2 `2 = r0
by A3, A6;
then A13:
p1 `2 = p2 `2
by A3, A5;
consider f2 being
Function of
I[01],
((TOP-REAL 2) | P2) such that A15:
f2 is
being_homeomorphism
and A16:
f2 . 0 = p1
and A17:
f2 . 1
= p2
by A8, TOPREAL1:def 1;
f2 is
continuous
by A15, TOPS_2:def 5;
then consider g2 being
Function of
I[01],
R^1 such that A18:
g2 is
continuous
and A19:
for
r being
Real for
q2 being
Point of
(TOP-REAL 2) st
r in the
carrier of
I[01] &
q2 = f2 . r holds
q2 `1 = g2 . r
by Th12;
A20:
[#] ((TOP-REAL 2) | P2) = P2
by PRE_TOPC:def 5;
1
in {0,1}
by TARSKI:def 2;
then A21:
1
in the
carrier of
I[01]
by A2, BORSUK_1:40, XBOOLE_0:def 3;
then A22:
p2 `1 = g2 . 1
by A17, A19;
0 in {0,1}
by TARSKI:def 2;
then A23:
0 in the
carrier of
I[01]
by A2, BORSUK_1:40, XBOOLE_0:def 3;
then
p1 `1 = g2 . 0
by A16, A19;
then consider r2 being
Real such that A24:
(
0 < r2 &
r2 < 1 )
and A25:
g2 . r2 = ((p1 `1) + (p2 `1)) / 2
by A18, A22, A14, Th9;
A26:
[.0,1.] = { r3 where r3 is Real : ( 0 <= r3 & r3 <= 1 ) }
by RCOMP_1:def 1;
then A27:
r2 in the
carrier of
I[01]
by A24, BORSUK_1:40;
dom f2 = the
carrier of
I[01]
by FUNCT_2:def 1;
then A28:
f2 . r2 in rng f2
by A27, FUNCT_1:def 3;
then A29:
f2 . r2 in P
by A9, A20, XBOOLE_0:def 3;
f2 . r2 in P2
by A28, A20;
then reconsider p4 =
f2 . r2 as
Point of
(TOP-REAL 2) ;
A30:
[#] ((TOP-REAL 2) | P1) = P1
by PRE_TOPC:def 5;
consider f1 being
Function of
I[01],
((TOP-REAL 2) | P1) such that A31:
f1 is
being_homeomorphism
and A32:
f1 . 0 = p1
and A33:
f1 . 1
= p2
by A7, TOPREAL1:def 1;
f1 is
continuous
by A31, TOPS_2:def 5;
then consider g1 being
Function of
I[01],
R^1 such that A34:
g1 is
continuous
and A35:
for
r being
Real for
q1 being
Point of
(TOP-REAL 2) st
r in the
carrier of
I[01] &
q1 = f1 . r holds
q1 `1 = g1 . r
by Th12;
A36:
p2 `1 = g1 . 1
by A33, A35, A21;
p1 `1 = g1 . 0
by A32, A35, A23;
then consider r1 being
Real such that A37:
(
0 < r1 &
r1 < 1 )
and A38:
g1 . r1 = ((p1 `1) + (p2 `1)) / 2
by A34, A36, A14, Th9;
A39:
r1 in the
carrier of
I[01]
by A37, A26, BORSUK_1:40;
then
r1 in dom f1
by FUNCT_2:def 1;
then A40:
f1 . r1 in rng f1
by FUNCT_1:def 3;
then
f1 . r1 in P1
by A30;
then reconsider p3 =
f1 . r1 as
Point of
(TOP-REAL 2) ;
f1 . r1 in P
by A9, A40, A30, XBOOLE_0:def 3;
then A41:
p3 `2 =
r0
by A3
.=
p4 `2
by A3, A29
;
p3 `1 =
((p1 `1) + (p2 `1)) / 2
by A35, A38, A39
.=
p4 `1
by A19, A25, A27
;
then
f1 . r1 = f2 . r2
by A41, TOPREAL3:6;
then A42:
f1 . r1 in P1 /\ P2
by A40, A30, A28, A20, XBOOLE_0:def 4;
now ( ( f1 . r1 = p1 & contradiction ) or ( f1 . r1 = p2 & contradiction ) )end; hence
contradiction
;
verum end;
hence
for r being Real ex p being Point of (TOP-REAL 2) st
( p in P & not p `2 = r )
; verum