:: deftheorem defines being_line EUCLID_4:def 2 :
for n being Nat
for A being Subset of (REAL n) holds
( A is being_line iff ex x1, x2 being Element of REAL n st
( x1 <> x2 & A = Line (x1,x2) ) );