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 that

A1: p2 in Q and

A2: P /\ Q is closed and

A3: P is_an_arc_of p1,p2 ; :: thesis: Last_Point (P,p1,p2,Q) = p2

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 = p2 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

then ( p2 in P /\ Q & P meets Q ) by A1, XBOOLE_0:def 4;

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

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 that

A1: p2 in Q and

A2: P /\ Q is closed and

A3: P is_an_arc_of p1,p2 ; :: thesis: Last_Point (P,p1,p2,Q) = p2

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 = p2 & 0 <= s2 & s2 <= 1 holds

for t being Real st 1 >= t & t > s2 holds

not g . t in Q

proof

p2 in P
by A3, TOPREAL1:1;
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 that

A5: g is being_homeomorphism and

g . 0 = p1 and

A6: ( g . 1 = p2 & g . s2 = p2 ) and

A7: ( 0 <= s2 & s2 <= 1 ) ; :: thesis: for t being Real st 1 >= t & t > s2 holds

not g . t in Q

A8: 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 A9: ( 1 >= t & t > s2 ) ; :: thesis: not g . t in Q

A10: dom g = [#] I[01] by A5, TOPS_2:def 5

.= the carrier of I[01] ;

then A11: 1 in dom g by BORSUK_1:43;

s2 in dom g by A7, A10, BORSUK_1:43;

hence not g . t in Q by A6, A11, A8, A9, FUNCT_1:def 4; :: thesis: verum

end;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 that

A5: g is being_homeomorphism and

g . 0 = p1 and

A6: ( g . 1 = p2 & g . s2 = p2 ) and

A7: ( 0 <= s2 & s2 <= 1 ) ; :: thesis: for t being Real st 1 >= t & t > s2 holds

not g . t in Q

A8: 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 A9: ( 1 >= t & t > s2 ) ; :: thesis: not g . t in Q

A10: dom g = [#] I[01] by A5, TOPS_2:def 5

.= the carrier of I[01] ;

then A11: 1 in dom g by BORSUK_1:43;

s2 in dom g by A7, A10, BORSUK_1:43;

hence not g . t in Q by A6, A11, A8, A9, FUNCT_1:def 4; :: thesis: verum

then ( p2 in P /\ Q & P meets Q ) by A1, XBOOLE_0:def 4;

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