let n be 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 p2,p1 & 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 p2,p1 & 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 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 ; :: thesis: P1 = P
P1 is_an_arc_of p1,p2 by A2, JORDAN5B:14;
hence P1 = P by A1, A3, JORDAN6:46; :: thesis: verum