let n be Nat; :: thesis: for A being Subset of (TOP-REAL n) st A is being_line holds

ex p1, p2 being Point of (TOP-REAL n) st

( p1 in A & p2 in A & p1 <> p2 )

let A be Subset of (TOP-REAL n); :: thesis: ( A is being_line implies ex p1, p2 being Point of (TOP-REAL n) st

( p1 in A & p2 in A & p1 <> p2 ) )

assume A is being_line ; :: thesis: ex p1, p2 being Point of (TOP-REAL n) st

( p1 in A & p2 in A & p1 <> p2 )

then consider p1, p2 being Point of (TOP-REAL n) such that

A1: p1 <> p2 and

A2: A = Line (p1,p2) ;

( p1 in A & p2 in A ) by A2, RLTOPSP1:72;

hence ex p1, p2 being Point of (TOP-REAL n) st

( p1 in A & p2 in A & p1 <> p2 ) by A1; :: thesis: verum

ex p1, p2 being Point of (TOP-REAL n) st

( p1 in A & p2 in A & p1 <> p2 )

let A be Subset of (TOP-REAL n); :: thesis: ( A is being_line implies ex p1, p2 being Point of (TOP-REAL n) st

( p1 in A & p2 in A & p1 <> p2 ) )

assume A is being_line ; :: thesis: ex p1, p2 being Point of (TOP-REAL n) st

( p1 in A & p2 in A & p1 <> p2 )

then consider p1, p2 being Point of (TOP-REAL n) such that

A1: p1 <> p2 and

A2: A = Line (p1,p2) ;

( p1 in A & p2 in A ) by A2, RLTOPSP1:72;

hence ex p1, p2 being Point of (TOP-REAL n) st

( p1 in A & p2 in A & p1 <> p2 ) by A1; :: thesis: verum