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

First_Point (P,p1,p2,Q) = p

let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p in P & P is_an_arc_of p1,p2 & Q = {p} implies First_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: First_Point (P,p1,p2,Q) = p

A4: P /\ {p} = {p} by A1, ZFMISC_1:46;

A5: 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 = p & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in {p}

A16: p in P /\ {p} by A4, TARSKI:def 1;

then P meets {p} ;

hence First_Point (P,p1,p2,Q) = p by A2, A3, A16, A15, A5, Def1; :: thesis: verum

First_Point (P,p1,p2,Q) = p

let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p in P & P is_an_arc_of p1,p2 & Q = {p} implies First_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: First_Point (P,p1,p2,Q) = p

A4: P /\ {p} = {p} by A1, ZFMISC_1:46;

A5: 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 = p & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= t & t < s2 holds

not g . t in {p}

proof

A15:
P /\ Q is closed
by A3, A4, PCOMPS_1:7;
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 = p & 0 <= s2 & s2 <= 1 holds

for t being Real st 0 <= 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 0 <= 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 0 <= t & t < s2 holds

not g . t in {p}

A10: g is one-to-one by A6, TOPS_2:def 5;

let t be Real; :: thesis: ( 0 <= t & t < s2 implies not g . t in {p} )

assume that

A11: 0 <= t and

A12: t < s2 ; :: thesis: not g . t in {p}

A13: dom g = the carrier of I[01] by A1, FUNCT_2:def 1;

t <= 1 by A9, A12, XXREAL_0:2;

then A14: t in dom g by A13, A11, BORSUK_1:43;

s2 in dom g by A8, A9, A13, BORSUK_1:43;

then g . t <> g . s2 by A10, A12, A14, FUNCT_1:def 4;

hence not g . t in {p} by A7, TARSKI:def 1; :: thesis: verum

end;for t being Real st 0 <= 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 0 <= 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 0 <= t & t < s2 holds

not g . t in {p}

A10: g is one-to-one by A6, TOPS_2:def 5;

let t be Real; :: thesis: ( 0 <= t & t < s2 implies not g . t in {p} )

assume that

A11: 0 <= t and

A12: t < s2 ; :: thesis: not g . t in {p}

A13: dom g = the carrier of I[01] by A1, FUNCT_2:def 1;

t <= 1 by A9, A12, XXREAL_0:2;

then A14: t in dom g by A13, A11, BORSUK_1:43;

s2 in dom g by A8, A9, A13, BORSUK_1:43;

then g . t <> g . s2 by A10, A12, A14, FUNCT_1:def 4;

hence not g . t in {p} by A7, TARSKI:def 1; :: thesis: verum

A16: p in P /\ {p} by A4, TARSKI:def 1;

then P meets {p} ;

hence First_Point (P,p1,p2,Q) = p by A2, A3, A16, A15, A5, Def1; :: thesis: verum