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;

per cases ( ss1 < ss2 or ss1 = ss2 or ss1 > ss2 ) by XXREAL_0:1;

suppose ss1 < ss2 ; :: thesis: IT1 = IT2

hence IT1 = IT2 by A5, A7, A10, A11, A12, A15, A18, A16, A21; :: thesis: verum

end;

suppose ss1 = ss2 ; :: thesis: IT1 = IT2

hence IT1 = IT2 by A15, A18; :: thesis: verum

end;

suppose ss1 > ss2 ; :: thesis: IT1 = IT2

hence IT1 = IT2 by A5, A8, A9, A11, A12, A15, A18, A20, A19; :: thesis: verum

end;

end;