let n be Nat; :: thesis: for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
P \ {p1,p2} <> {}
let P be Subset of (TOP-REAL n); :: thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
P \ {p1,p2} <> {}
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 implies P \ {p1,p2} <> {} )
assume P is_an_arc_of p1,p2 ; :: thesis: P \ {p1,p2} <> {}
then consider p3 being Point of (TOP-REAL n) such that
A1: p3 in P and
A2: p3 <> p1 and
A3: p3 <> p2 by Th42;
not p3 in {p1,p2} by A2, A3, TARSKI:def 2;
hence P \ {p1,p2} <> {} by A1, XBOOLE_0:def 5; :: thesis: verum