let n be Element of NAT ; for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st A is_an_arc_of p,q holds
not A \ {p} is empty
let A be Subset of (TOP-REAL n); for p, q being Point of (TOP-REAL n) st A is_an_arc_of p,q holds
not A \ {p} is empty
let p, q be Point of (TOP-REAL n); ( A is_an_arc_of p,q implies not A \ {p} is empty )
assume
A is_an_arc_of p,q
; not A \ {p} is empty
then A1:
A \ {p,q} <> {}
by JORDAN6:43;
{p} c= {p,q}
by ZFMISC_1:7;
hence
not A \ {p} is empty
by A1, XBOOLE_1:3, XBOOLE_1:34; verum