:: deftheorem Def3 defines being_line AFF_1:def 3 :
for AS being AffinSpace
for A being Subset of AS holds
( A is being_line iff ex a, b being Element of AS st
( a <> b & A = Line (a,b) ) );