let n be Nat; :: thesis: for P1, P2 being Subset of ()
for p1, p2 being Point of () st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds
P1 = P2

let P1, P2 be Subset of (); :: thesis: for p1, p2 being Point of () st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds
P1 = P2

let p1, p2 be Point of (); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 implies P1 = P2 )
assume that
A1: P1 is_an_arc_of p1,p2 and
A2: P2 is_an_arc_of p1,p2 and
A3: P1 c= P2 ; :: thesis: P1 = P2
reconsider P19 = P1, P29 = P2 as non empty Subset of () by ;
now :: thesis: not P2 \ P1 <> {}
assume A4: P2 \ P1 <> {} ; :: thesis: contradiction
set p = the Element of P2 \ P1;
A5: the Element of P2 \ P1 in P2 by ;
A6: not the Element of P2 \ P1 in P1 by ;
consider f1 being Function of I[01],(() | P19) such that
A7: f1 is being_homeomorphism and
A8: f1 . 0 = p1 and
A9: f1 . 1 = p2 by ;
A10: f1 is continuous by ;
consider f2 being Function of I[01],(() | P29) such that
A11: f2 is being_homeomorphism and
A12: f2 . 0 = p1 and
A13: f2 . 1 = p2 by ;
reconsider f4 = f2 as Function ;
A14: f2 is one-to-one by ;
A15: rng f2 = [#] (() | P2) by ;
A16: f2 " is being_homeomorphism by ;
then A17: dom (f2 ") = [#] (() | P2) by TOPS_2:def 5
.= P2 by PRE_TOPC:def 5 ;
f2 " is continuous by ;
then consider h being Function of I[01],I[01] such that
A18: h = (f2 ") * f1 and
A19: h is continuous by ;
reconsider h1 = h as Function of (),R^1 by ;
for F1 being Subset of R^1 st F1 is closed holds
h1 " F1 is closed
proof
let F1 be Subset of R^1; :: thesis: ( F1 is closed implies h1 " F1 is closed )
assume A20: F1 is closed ; :: thesis: h1 " F1 is closed
reconsider K = the carrier of I[01] as Subset of R^1 by ;
A21: I[01] = R^1 | K by ;
reconsider P3 = F1 /\ K as Subset of (R^1 | K) by TOPS_2:29;
A22: P3 is closed by ;
h1 " K = the carrier of I[01] by FUNCT_2:40
.= dom h1 by FUNCT_2:def 1 ;
then h1 " F1 = (h1 " F1) /\ (h1 " K) by
.= h " P3 by FUNCT_1:68 ;
hence h1 " F1 is closed by ; :: thesis: verum
end;
then reconsider g = h1 as continuous Function of (),R^1 by PRE_TOPC:def 6;
A23: dom f1 = [#] I[01] by
.= [.0,1.] by BORSUK_1:40 ;
then A24: 0 in dom f1 by XXREAL_1:1;
A25: 1 in dom f1 by ;
A26: g . 0 = (f2 ") . p1 by ;
A27: g . 1 = (f2 ") . p2 by ;
A28: dom f2 = [#] I[01] by
.= [.0,1.] by BORSUK_1:40 ;
then A29: 0 in dom f2 by XXREAL_1:1;
A30: 1 in dom f2 by ;
A31: f2 is onto by ;
then A32: (f2 ") . p1 = (f4 ") . p1 by ;
A33: (f2 ") . p2 = (f4 ") . p2 by ;
A34: g . 0 = 0 by ;
A35: g . 1 = 1 by ;
the Element of P2 \ P1 in the carrier of (() | P29) by ;
then A36: (f2 ") . the Element of P2 \ P1 in the carrier of I[01] by FUNCT_2:5;
A37: now :: thesis: not (f2 ") . the Element of P2 \ P1 in rng g
assume (f2 ") . the Element of P2 \ P1 in rng g ; :: thesis: contradiction
then consider x being object such that
A38: x in dom g and
A39: (f2 ") . the Element of P2 \ P1 = g . x by FUNCT_1:def 3;
A40: (f2 ") . the Element of P2 \ P1 = (f2 ") . (f1 . x) by ;
A41: x in dom f1 by ;
A42: f1 . x in dom (f2 ") by ;
f2 " is one-to-one by ;
then the Element of P2 \ P1 = f1 . x by ;
then A43: the Element of P2 \ P1 in rng f1 by ;
rng f1 = [#] (() | P1) by
.= P1 by PRE_TOPC:def 5 ;
hence contradiction by A4, A43, XBOOLE_0:def 5; :: thesis: verum
end;
reconsider r = (f2 ") . the Element of P2 \ P1 as Real ;
A44: rng f2 = [#] (() | P2) by
.= P2 by PRE_TOPC:def 5 ;
A45: r <= 1 by ;
A46: now :: thesis: not r = 0
assume A47: r = 0 ; :: thesis: contradiction
f2 . r = f4 . ((f4 ") . the Element of P2 \ P1) by
.= the Element of P2 \ P1 by ;
hence contradiction by A1, A6, A12, A47, TOPREAL1:1; :: thesis: verum
end;
A48: now :: thesis: not r = 1
assume A49: r = 1 ; :: thesis: contradiction
f2 . r = f4 . ((f4 ") . the Element of P2 \ P1) by
.= the Element of P2 \ P1 by ;
hence contradiction by A1, A6, A13, A49, TOPREAL1:1; :: thesis: verum
end;
A50: 0 < r by ;
r < 1 by ;
then consider rc being Real such that
A51: g . rc = r and
A52: 0 < rc and
A53: rc < 1 by ;
the carrier of (() | P1) = [#] (() | P1)
.= P1 by PRE_TOPC:def 5 ;
then rng f1 c= dom (f2 ") by ;
then dom g = dom f1 by
.= [#] I[01] by
.= [.0,1.] by BORSUK_1:40 ;
then rc in dom g by ;
hence contradiction by A37, A51, FUNCT_1:def 3; :: thesis: verum
end;
then P2 c= P1 by XBOOLE_1:37;
hence P1 = P2 by A3; :: thesis: verum