theorem Th20: :: AFF_1:21
for AS being AffinSpace
for a, b, c being Element of AS holds
( LIN a,b,c iff ex A being Subset of AS st
( A is being_line & a in A & b in A & c in A ) )