let P, Q be Subset of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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); :: thesis: 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
let s2 be Real; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: ( 0 <= t & t < s2 implies not g . t in Q )
assume A10: ( 0 <= t & t < s2 ) ; :: thesis: 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; :: thesis: 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; :: thesis: verum