let P, Q be Subset of (TOP-REAL 2); for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds
First_Point (P,p1,p2,Q) = p
let p, p1, p2 be Point of (TOP-REAL 2); ( p in P & P is_an_arc_of p1,p2 & Q = {p} implies First_Point (P,p1,p2,Q) = p )
assume that
A1:
p in P
and
A2:
P is_an_arc_of p1,p2
and
A3:
Q = {p}
; First_Point (P,p1,p2,Q) = p
A4:
P /\ {p} = {p}
by A1, ZFMISC_1:46;
A5:
for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in {p}
proof
let g be
Function of
I[01],
((TOP-REAL 2) | P);
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in {p}let s2 be
Real;
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds
not g . t in {p} )
assume that A6:
g is
being_homeomorphism
and
g . 0 = p1
and
g . 1
= p2
and A7:
g . s2 = p
and A8:
0 <= s2
and A9:
s2 <= 1
;
for t being Real st 0 <= t & t < s2 holds
not g . t in {p}
A10:
g is
one-to-one
by A6, TOPS_2:def 5;
let t be
Real;
( 0 <= t & t < s2 implies not g . t in {p} )
assume that A11:
0 <= t
and A12:
t < s2
;
not g . t in {p}
A13:
dom g = the
carrier of
I[01]
by A1, FUNCT_2:def 1;
t <= 1
by A9, A12, XXREAL_0:2;
then A14:
t in dom g
by A13, A11, BORSUK_1:43;
s2 in dom g
by A8, A9, A13, BORSUK_1:43;
then
g . t <> g . s2
by A10, A12, A14, FUNCT_1:def 4;
hence
not
g . t in {p}
by A7, TARSKI:def 1;
verum
end;
A15:
P /\ Q is closed
by A3, A4, PCOMPS_1:7;
A16:
p in P /\ {p}
by A4, TARSKI:def 1;
then
P meets {p}
;
hence
First_Point (P,p1,p2,Q) = p
by A2, A3, A16, A15, A5, Def1; verum