let n be Nat; :: thesis: for p1 being Point of (TOP-REAL n)
for A being Subset of (TOP-REAL n) st A is being_line holds
ex p2 being Point of (TOP-REAL n) st
( p1 <> p2 & p2 in A )
let p1 be Point of (TOP-REAL n); :: thesis: for A being Subset of (TOP-REAL n) st A is being_line holds
ex p2 being Point of (TOP-REAL n) st
( p1 <> p2 & p2 in A )
let A be Subset of (TOP-REAL n); :: thesis: ( A is being_line implies ex p2 being Point of (TOP-REAL n) st
( p1 <> p2 & p2 in A ) )
assume A is being_line ; :: thesis: ex p2 being Point of (TOP-REAL n) st
( p1 <> p2 & p2 in A )
then consider q1, q2 being Point of (TOP-REAL n) such that
A1: q1 in A and
A2: ( q2 in A & q1 <> q2 ) by Th44;
( p1 = q1 implies ( p1 <> q2 & q2 in A ) ) by A2;
hence ex p2 being Point of (TOP-REAL n) st
( p1 <> p2 & p2 in A ) by A1; :: thesis: verum