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 )
A3:
( P /\ Q c= Q & P /\ Q c= P )
by XBOOLE_1:17;
assume A4:
( IT1 in P /\ Q & ( 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 A5:
( IT2 in P /\ Q & ( 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
A6:
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 )
by A1, TOPREAL1:def 2;
A7: rng g =
[#] ((TOP-REAL 2) | P)
by A6, TOPS_2:def 5
.=
P
by PRE_TOPC:def 10
;
A8: dom g =
[#] I[01]
by A6, TOPS_2:def 5
.=
the carrier of I[01]
;
consider ss1 being set such that
A9:
( ss1 in dom g & g . ss1 = IT1 )
by A3, A4, A7, FUNCT_1:def 5;
reconsider ss1 = ss1 as Real by A8, A9, BORSUK_1:83;
consider ss2 being set such that
A10:
( ss2 in dom g & g . ss2 = IT2 )
by A3, A5, A7, FUNCT_1:def 5;
reconsider ss2 = ss2 as Real by A8, A10, BORSUK_1:83;
A11:
( 0 <= ss1 & ss1 <= 1 & 0 <= ss2 & ss2 <= 1 )
by A9, A10, BORSUK_1:86;