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