let n be Element of NAT ; :: thesis: 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 p1,p2 & P1 c= P holds
P1 = P
let p1, p2 be Point of (TOP-REAL n); :: thesis: for P, P1 being non empty Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 & P1 is_an_arc_of p1,p2 & P1 c= P holds
P1 = P
let P, P1 be non empty Subset of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 & P1 is_an_arc_of p1,p2 & P1 c= P implies P1 = P )
assume A1: ( P is_an_arc_of p1,p2 & P1 is_an_arc_of p1,p2 & P1 c= P ) ; :: thesis: P1 = P
then P1 is_an_arc_of p2,p1 by JORDAN5B:14;
hence P1 = P by A1, TOPMETR3:18; :: thesis: verum