theorem :: AFF_1:26
for AS being AffinSpace
for A being Subset of AS st ex a, b being Element of AS st a,b // A holds
A is being_line ;