let P1, P2, P3 be Subset of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P3 is_an_arc_of p1,p2 & P2 /\ P3 = {p1,p2} & P1 c= P2 \/ P3 & not P1 = P2 holds
P1 = P3
set P = P2 \/ P3;
A1: the carrier of ((TOP-REAL 2) | (P2 \/ P3)) = [#] ((TOP-REAL 2) | (P2 \/ P3))
.= P2 \/ P3 by PRE_TOPC:def 5 ;
then reconsider U2 = P2 as Subset of ((TOP-REAL 2) | (P2 \/ P3)) by XBOOLE_1:7;
reconsider U3 = P3 as Subset of ((TOP-REAL 2) | (P2 \/ P3)) by A1, XBOOLE_1:7;
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P3 is_an_arc_of p1,p2 & P2 /\ P3 = {p1,p2} & P1 c= P2 \/ P3 & not P1 = P2 implies P1 = P3 )
assume that
A2: P1 is_an_arc_of p1,p2 and
A3: P2 is_an_arc_of p1,p2 and
A4: P3 is_an_arc_of p1,p2 ; :: thesis: ( not P2 /\ P3 = {p1,p2} or not P1 c= P2 \/ P3 or P1 = P2 or P1 = P3 )
consider f being Function of I[01],((TOP-REAL 2) | P1) such that
A5: f is being_homeomorphism and
A6: ( f . 0 = p1 & f . 1 = p2 ) by A2;
A7: f is one-to-one by A5;
U2 = P2 /\ (P2 \/ P3) by XBOOLE_1:7, XBOOLE_1:28;
then A8: U2 is closed by A3, JORDAN6:2, JORDAN6:11;
A9: rng f = [#] ((TOP-REAL 2) | P1) by A5
.= P1 by PRE_TOPC:def 5 ;
p1 in P2 by A3, TOPREAL1:1;
then reconsider Q = P2 \/ P3 as non empty Subset of (Euclid 2) by TOPREAL3:8;
assume that
A10: P2 /\ P3 = {p1,p2} and
A11: P1 c= P2 \/ P3 ; :: thesis: ( P1 = P2 or P1 = P3 )
A12: ( p2 in P2 /\ P3 & p1 in P2 /\ P3 ) by A10, TARSKI:def 2;
U3 = P3 /\ (P2 \/ P3) by XBOOLE_1:7, XBOOLE_1:28;
then A13: U3 is closed by A4, JORDAN6:2, JORDAN6:11;
A14: f is continuous by A5;
A15: dom f = [#] I[01] by A5;
per cases ( for r being Real st 0 < r & r < 1 holds
f . r in P3 or ex r being Real st
( 0 < r & r < 1 & not f . r in P3 ) ) ;
suppose A16: for r being Real st 0 < r & r < 1 holds
f . r in P3 ; :: thesis: ( P1 = P2 or P1 = P3 )
P1 c= P3
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in P1 or y in P3 )
assume y in P1 ; :: thesis: y in P3
then consider x being object such that
A17: x in dom f and
A18: y = f . x by A9, FUNCT_1:def 3;
reconsider r = x as Real by A17;
r <= 1 by A17, BORSUK_1:40, XXREAL_1:1;
then ( r = 0 or r = 1 or ( 0 < r & r < 1 ) ) by A17, BORSUK_1:40, XXREAL_0:1, XXREAL_1:1;
hence y in P3 by A12, A6, A16, A18, XBOOLE_0:def 4; :: thesis: verum
end;
hence ( P1 = P2 or P1 = P3 ) by A2, A4, JORDAN6:46; :: thesis: verum
end;
suppose A19: ex r being Real st
( 0 < r & r < 1 & not f . r in P3 ) ; :: thesis: ( P1 = P2 or P1 = P3 )
now :: thesis: ( ( ( for r being Real st 0 < r & r < 1 holds
f . r in P2 ) & ( P1 = P2 or P1 = P3 ) ) or ( ex r being Real st
( 0 < r & r < 1 & not f . r in P2 ) & contradiction ) )
per cases ( for r being Real st 0 < r & r < 1 holds
f . r in P2 or ex r being Real st
( 0 < r & r < 1 & not f . r in P2 ) ) ;
case A20: for r being Real st 0 < r & r < 1 holds
f . r in P2 ; :: thesis: ( P1 = P2 or P1 = P3 )
P1 c= P2
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in P1 or y in P2 )
assume y in P1 ; :: thesis: y in P2
then consider x being object such that
A21: x in dom f and
A22: y = f . x by A9, FUNCT_1:def 3;
reconsider r = x as Real by A21;
r <= 1 by A21, BORSUK_1:40, XXREAL_1:1;
then ( ( 0 < r & r < 1 ) or r = 0 or r = 1 ) by A21, BORSUK_1:40, XXREAL_0:1, XXREAL_1:1;
hence y in P2 by A12, A6, A20, A22, XBOOLE_0:def 4; :: thesis: verum
end;
hence ( P1 = P2 or P1 = P3 ) by A2, A3, JORDAN6:46; :: thesis: verum
end;
case ex r being Real st
( 0 < r & r < 1 & not f . r in P2 ) ; :: thesis: contradiction
then consider r2 being Real such that
A23: 0 < r2 and
A24: r2 < 1 and
A25: not f . r2 in P2 ;
r2 in [.0,1.] by A23, A24, XXREAL_1:1;
then f . r2 in rng f by A15, BORSUK_1:40, FUNCT_1:def 3;
then A26: f . r2 in P3 by A11, A9, A25, XBOOLE_0:def 3;
consider r1 being Real such that
A27: 0 < r1 and
A28: r1 < 1 and
A29: not f . r1 in P3 by A19;
r1 in [.0,1.] by A27, A28, XXREAL_1:1;
then A30: f . r1 in rng f by A15, BORSUK_1:40, FUNCT_1:def 3;
then A31: f . r1 in P2 by A11, A9, A29, XBOOLE_0:def 3;
now :: thesis: contradiction
per cases ( r1 <= r2 or r1 > r2 ) ;
suppose A32: r1 <= r2 ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( r1 = r2 or r1 < r2 ) by A32, XXREAL_0:1;
suppose A33: r1 < r2 ; :: thesis: contradiction
A34: the carrier of ((TOP-REAL 2) | P1) = [#] ((TOP-REAL 2) | P1)
.= P1 by PRE_TOPC:def 5 ;
the carrier of ((TOP-REAL 2) | (P2 \/ P3)) = [#] ((TOP-REAL 2) | (P2 \/ P3))
.= P2 \/ P3 by PRE_TOPC:def 5 ;
then rng f c= the carrier of ((TOP-REAL 2) | (P2 \/ P3)) by A11, A34;
then reconsider g = f as Function of I[01],((TOP-REAL 2) | (P2 \/ P3)) by A15, FUNCT_2:2;
P2 \/ P3 = P1 \/ (P2 \/ P3) by A11, XBOOLE_1:12;
then A35: (TOP-REAL 2) | P1 is SubSpace of (TOP-REAL 2) | (P2 \/ P3) by TOPMETR:4;
( U2 \/ U3 = the carrier of ((Euclid 2) | Q) & (TOP-REAL 2) | (P2 \/ P3) = TopSpaceMetr ((Euclid 2) | Q) ) by EUCLID:63, TOPMETR:def 2;
then consider r0 being Real such that
A36: r1 <= r0 and
A37: r0 <= r2 and
A38: g . r0 in U2 /\ U3 by A14, A8, A13, A24, A27, A26, A31, A33, A35, PRE_TOPC:26, TOPMETR3:13;
r0 < 1 by A24, A37, XXREAL_0:2;
then A39: r0 in dom f by A15, A27, A36, BORSUK_1:40, XXREAL_1:1;
A40: ( 0 in dom f & 1 in dom f ) by A15, BORSUK_1:40, XXREAL_1:1;
( g . r0 = p1 or g . r0 = p2 ) by A10, A38, TARSKI:def 2;
hence contradiction by A6, A7, A24, A27, A36, A37, A39, A40, FUNCT_1:def 4; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A41: r1 > r2 ; :: thesis: contradiction
A42: the carrier of ((TOP-REAL 2) | P1) = [#] ((TOP-REAL 2) | P1)
.= P1 by PRE_TOPC:def 5 ;
the carrier of ((TOP-REAL 2) | (P2 \/ P3)) = [#] ((TOP-REAL 2) | (P2 \/ P3))
.= P2 \/ P3 by PRE_TOPC:def 5 ;
then rng f c= the carrier of ((TOP-REAL 2) | (P2 \/ P3)) by A11, A42;
then reconsider g = f as Function of I[01],((TOP-REAL 2) | (P2 \/ P3)) by A15, FUNCT_2:2;
P2 \/ P3 = P1 \/ (P2 \/ P3) by A11, XBOOLE_1:12;
then A43: (TOP-REAL 2) | P1 is SubSpace of (TOP-REAL 2) | (P2 \/ P3) by TOPMETR:4;
( U2 \/ U3 = the carrier of ((Euclid 2) | Q) & (TOP-REAL 2) | (P2 \/ P3) = TopSpaceMetr ((Euclid 2) | Q) ) by EUCLID:63, TOPMETR:def 2;
then consider r0 being Real such that
A44: r2 <= r0 and
A45: r0 <= r1 and
A46: g . r0 in U2 /\ U3 by A14, A8, A13, A23, A28, A26, A31, A41, A43, PRE_TOPC:26, TOPMETR3:13;
r0 < 1 by A28, A45, XXREAL_0:2;
then A47: r0 in dom f by A15, A23, A44, BORSUK_1:40, XXREAL_1:1;
A48: ( 0 in dom f & 1 in dom f ) by A15, BORSUK_1:40, XXREAL_1:1;
( g . r0 = p1 or g . r0 = p2 ) by A10, A46, TARSKI:def 2;
hence contradiction by A6, A7, A23, A28, A44, A45, A47, A48, FUNCT_1:def 4; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence ( P1 = P2 or P1 = P3 ) ; :: thesis: verum
end;
end;