theorem :: AFF_1:24

for AS being AffinSpace
for a, b being Element of AS
for A being Subset of AS holds
( a <> b & A = Line (a,b) iff ( A is being_line & a in A & b in A & a <> b ) ) by Lm6, Th14;