let n be Nat; 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); 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); ( P is_an_arc_of p1,p2 implies P \ {p1,p2} <> {} )
assume
P is_an_arc_of p1,p2
; 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; verum