:: deftheorem defines being_line EUCLID_4:def 4 :
for n being Nat
for A being Subset of (TOP-REAL n) holds
( A is being_line iff ex p1, p2 being Point of (TOP-REAL n) st
( p1 <> p2 & A = Line (p1,p2) ) );