let n be Nat; for p1, p2 being Point of (TOP-REAL n)
for P, P1 being non empty Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 & P1 is_an_arc_of p2,p1 & P1 c= P holds
P1 = P
let p1, p2 be Point of (TOP-REAL n); for P, P1 being non empty Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 & P1 is_an_arc_of p2,p1 & P1 c= P holds
P1 = P
let P, P1 be non empty Subset of (TOP-REAL n); ( P is_an_arc_of p1,p2 & P1 is_an_arc_of p2,p1 & P1 c= P implies P1 = P )
assume that
A1:
P is_an_arc_of p1,p2
and
A2:
P1 is_an_arc_of p2,p1
and
A3:
P1 c= P
; P1 = P
P1 is_an_arc_of p1,p2
by A2, JORDAN5B:14;
hence
P1 = P
by A1, A3, JORDAN6:46; verum