:: deftheorem Def15 defines being_line RLTOPSP1:def 15 :
for V being RealLinearSpace
for A being Subset of V holds
( A is being_line iff ex x1, x2 being Element of V st A = Line (x1,x2) );