let n be Element of NAT ; :: thesis: 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); :: thesis: 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); :: thesis: ( A is_an_arc_of p,q implies not A \ {p} is empty )
assume A is_an_arc_of p,q ; :: thesis: 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; :: thesis: verum