let q1, q2 be Point of (TOP-REAL 2); for Q, P being non empty Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | Q),((TOP-REAL 2) | P) st f is being_homeomorphism & Q is_an_arc_of q1,q2 holds
for p1, p2 being Point of (TOP-REAL 2) st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2
let Q, P be non empty Subset of (TOP-REAL 2); for f being Function of ((TOP-REAL 2) | Q),((TOP-REAL 2) | P) st f is being_homeomorphism & Q is_an_arc_of q1,q2 holds
for p1, p2 being Point of (TOP-REAL 2) st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2
let f be Function of ((TOP-REAL 2) | Q),((TOP-REAL 2) | P); ( f is being_homeomorphism & Q is_an_arc_of q1,q2 implies for p1, p2 being Point of (TOP-REAL 2) st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2 )
assume that
A1:
f is being_homeomorphism
and
A2:
Q is_an_arc_of q1,q2
; for p1, p2 being Point of (TOP-REAL 2) st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2
let p1, p2 be Point of (TOP-REAL 2); ( p1 = f . q1 & p2 = f . q2 implies P is_an_arc_of p1,p2 )
assume that
A3:
p1 = f . q1
and
A4:
p2 = f . q2
; P is_an_arc_of p1,p2
reconsider f = f as Function of ((TOP-REAL 2) | Q),((TOP-REAL 2) | P) ;
consider f1 being Function of I[01],((TOP-REAL 2) | Q) such that
A5:
f1 is being_homeomorphism
and
A6:
f1 . 0 = q1
and
A7:
f1 . 1 = q2
by A2, TOPREAL1:def 1;
set g1 = f * f1;
A8:
dom f1 = the carrier of I[01]
by FUNCT_2:def 1;
then
0 in dom f1
by BORSUK_1:40, XXREAL_1:1;
then A9:
(f * f1) . 0 = p1
by A3, A6, FUNCT_1:13;
1 in dom f1
by A8, BORSUK_1:40, XXREAL_1:1;
then A10:
(f * f1) . 1 = p2
by A4, A7, FUNCT_1:13;
f * f1 is being_homeomorphism
by A1, A5, TOPS_2:57;
hence
P is_an_arc_of p1,p2
by A9, A10, TOPREAL1:def 1; verum