let P, Q be Subset of (TOP-REAL 2); for p1, p2 being Point of (TOP-REAL 2) st p1 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
First_Point (P,p1,p2,Q) = p1
let p1, p2 be Point of (TOP-REAL 2); ( p1 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 implies First_Point (P,p1,p2,Q) = p1 )
assume that
A1:
p1 in Q
and
A2:
P /\ Q is closed
and
A3:
P is_an_arc_of p1,p2
; First_Point (P,p1,p2,Q) = p1
A4:
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 = p1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
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 = p1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Qlet s2 be
Real;
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p1 & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds
not g . t in Q )
assume that A5:
g is
being_homeomorphism
and A6:
g . 0 = p1
and
g . 1
= p2
and A7:
g . s2 = p1
and A8:
(
0 <= s2 &
s2 <= 1 )
;
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
A9:
g is
one-to-one
by A5, TOPS_2:def 5;
let t be
Real;
( 0 <= t & t < s2 implies not g . t in Q )
assume A10:
(
0 <= t &
t < s2 )
;
not g . t in Q
A11:
dom g =
[#] I[01]
by A5, TOPS_2:def 5
.=
the
carrier of
I[01]
;
then A12:
0 in dom g
by BORSUK_1:43;
s2 in dom g
by A8, A11, BORSUK_1:43;
hence
not
g . t in Q
by A6, A7, A12, A9, A10, FUNCT_1:def 4;
verum
end;
p1 in P
by A3, TOPREAL1:1;
then
( p1 in P /\ Q & P meets Q )
by A1, XBOOLE_0:def 4;
hence
First_Point (P,p1,p2,Q) = p1
by A2, A3, A4, Def1; verum