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

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