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