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

end;

hence Last_Point P,p1,p2,Q = p2 by A1, A3, A4, Def2; :: thesis: verum