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

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