let IT1, IT2 be Point of (TOP-REAL 2); :: thesis: ( IT1 in P /\ Q & ( 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 = IT1 & 0 <= s2 & s2 <= 1 holds

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

not g . t in Q ) & IT2 in P /\ Q & ( 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 = IT2 & 0 <= s2 & s2 <= 1 holds

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

not g . t in Q ) implies IT1 = IT2 )

A5: P /\ Q c= Q by XBOOLE_1:17;

A6: P /\ Q c= P by XBOOLE_1:17;

assume that

A7: IT1 in P /\ Q and

A8: for g1 being Function of I[01],((TOP-REAL 2) | P)

for s1 being Real st g1 is being_homeomorphism & g1 . 0 = p1 & g1 . 1 = p2 & g1 . s1 = IT1 & 0 <= s1 & s1 <= 1 holds

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

not g1 . t in Q ; :: thesis: ( not IT2 in P /\ Q or ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st

( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT2 & 0 <= s2 & s2 <= 1 & ex t being Real st

( 0 <= t & t < s2 & g . t in Q ) ) or IT1 = IT2 )

assume that

A9: IT2 in P /\ Q and

A10: for g2 being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g2 is being_homeomorphism & g2 . 0 = p1 & g2 . 1 = p2 & g2 . s2 = IT2 & 0 <= s2 & s2 <= 1 holds

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

not g2 . t in Q ; :: thesis: IT1 = IT2

consider g being Function of I[01],((TOP-REAL 2) | P) such that

A11: g is being_homeomorphism and

A12: ( g . 0 = p1 & g . 1 = p2 ) by A2, TOPREAL1:def 1;

A13: rng g = [#] ((TOP-REAL 2) | P) by A11, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

then consider ss1 being object such that

A14: ss1 in dom g and

A15: g . ss1 = IT1 by A6, A7, FUNCT_1:def 3;

reconsider ss1 = ss1 as Real by A14, BORSUK_1:40;

A16: 0 <= ss1 by A14, BORSUK_1:43;

consider ss2 being object such that

A17: ss2 in dom g and

A18: g . ss2 = IT2 by A6, A9, A13, FUNCT_1:def 3;

reconsider ss2 = ss2 as Real by A17, BORSUK_1:40;

A19: 0 <= ss2 by A17, BORSUK_1:43;

A20: ss1 <= 1 by A14, BORSUK_1:43;

A21: ss2 <= 1 by A17, BORSUK_1:43;

for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT1 & 0 <= s2 & s2 <= 1 holds

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

not g . t in Q ) & IT2 in P /\ Q & ( 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 = IT2 & 0 <= s2 & s2 <= 1 holds

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

not g . t in Q ) implies IT1 = IT2 )

A5: P /\ Q c= Q by XBOOLE_1:17;

A6: P /\ Q c= P by XBOOLE_1:17;

assume that

A7: IT1 in P /\ Q and

A8: for g1 being Function of I[01],((TOP-REAL 2) | P)

for s1 being Real st g1 is being_homeomorphism & g1 . 0 = p1 & g1 . 1 = p2 & g1 . s1 = IT1 & 0 <= s1 & s1 <= 1 holds

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

not g1 . t in Q ; :: thesis: ( not IT2 in P /\ Q or ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st

( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT2 & 0 <= s2 & s2 <= 1 & ex t being Real st

( 0 <= t & t < s2 & g . t in Q ) ) or IT1 = IT2 )

assume that

A9: IT2 in P /\ Q and

A10: for g2 being Function of I[01],((TOP-REAL 2) | P)

for s2 being Real st g2 is being_homeomorphism & g2 . 0 = p1 & g2 . 1 = p2 & g2 . s2 = IT2 & 0 <= s2 & s2 <= 1 holds

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

not g2 . t in Q ; :: thesis: IT1 = IT2

consider g being Function of I[01],((TOP-REAL 2) | P) such that

A11: g is being_homeomorphism and

A12: ( g . 0 = p1 & g . 1 = p2 ) by A2, TOPREAL1:def 1;

A13: rng g = [#] ((TOP-REAL 2) | P) by A11, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

then consider ss1 being object such that

A14: ss1 in dom g and

A15: g . ss1 = IT1 by A6, A7, FUNCT_1:def 3;

reconsider ss1 = ss1 as Real by A14, BORSUK_1:40;

A16: 0 <= ss1 by A14, BORSUK_1:43;

consider ss2 being object such that

A17: ss2 in dom g and

A18: g . ss2 = IT2 by A6, A9, A13, FUNCT_1:def 3;

reconsider ss2 = ss2 as Real by A17, BORSUK_1:40;

A19: 0 <= ss2 by A17, BORSUK_1:43;

A20: ss1 <= 1 by A14, BORSUK_1:43;

A21: ss2 <= 1 by A17, BORSUK_1:43;