let P, Q be Subset of (); :: thesis: for p, p1, p2 being Point of () st p in P & P is_an_arc_of p1,p2 & Q = {p} holds
Last_Point (P,p1,p2,Q) = p

let p, p1, p2 be Point of (); :: thesis: ( p in P & P is_an_arc_of p1,p2 & Q = {p} implies Last_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} ; :: thesis: Last_Point (P,p1,p2,Q) = p
A4: P /\ {p} = {p} by ;
A5: for g being Function of I,(() | 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 1 >= t & t > s2 holds
not g . t in {p}
proof
let g be Function of I,(() | P); :: thesis: 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 1 >= t & t > s2 holds
not g . t in {p}

let s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= 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 ; :: thesis: for t being Real st 1 >= t & t > s2 holds
not g . t in {p}

A10: g is one-to-one by ;
A11: dom g = the carrier of I by ;
then A12: s2 in dom g by ;
let t be Real; :: thesis: ( 1 >= t & t > s2 implies not g . t in {p} )
assume that
A13: 1 >= t and
A14: t > s2 ; :: thesis: not g . t in {p}
t in dom g by ;
then g . t <> g . s2 by ;
hence not g . t in {p} by ; :: thesis: verum
end;
A15: P /\ Q is closed by ;
A16: p in P /\ {p} by ;
then P meets {p} ;
hence Last_Point (P,p1,p2,Q) = p by A2, A3, A16, A15, A5, Def2; :: thesis: verum