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

ex x1, x2 being Element of REAL n st

( x1 in A & x2 in A & x1 <> x2 )

let A be Subset of (REAL n); :: thesis: ( A is being_line implies ex x1, x2 being Element of REAL n st

( x1 in A & x2 in A & x1 <> x2 ) )

assume A is being_line ; :: thesis: ex x1, x2 being Element of REAL n st

( x1 in A & x2 in A & x1 <> x2 )

then consider x1, x2 being Element of REAL n such that

A1: x1 <> x2 and

A2: A = Line (x1,x2) ;

( x1 in A & x2 in A ) by A2, Th9;

hence ex x1, x2 being Element of REAL n st

( x1 in A & x2 in A & x1 <> x2 ) by A1; :: thesis: verum

ex x1, x2 being Element of REAL n st

( x1 in A & x2 in A & x1 <> x2 )

let A be Subset of (REAL n); :: thesis: ( A is being_line implies ex x1, x2 being Element of REAL n st

( x1 in A & x2 in A & x1 <> x2 ) )

assume A is being_line ; :: thesis: ex x1, x2 being Element of REAL n st

( x1 in A & x2 in A & x1 <> x2 )

then consider x1, x2 being Element of REAL n such that

A1: x1 <> x2 and

A2: A = Line (x1,x2) ;

( x1 in A & x2 in A ) by A2, Th9;

hence ex x1, x2 being Element of REAL n st

( x1 in A & x2 in A & x1 <> x2 ) by A1; :: thesis: verum