let n be Element of 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 & p3 <> p1 & p3 <> p2 ) by Th55;
not p3 in {p1,p2} by A1, TARSKI:def 2;
hence P \ {p1,p2} <> {} by A1, XBOOLE_0:def 5; :: thesis: verum