theorem Th1: :: AFF_4:1

for AS being AffinSpace
for a, b, a9, p being Element of AS st ( LIN p,a,a9 or LIN p,a9,a ) & p <> a holds
ex b9 being Element of AS st
( LIN p,b,b9 & a,b // a9,b9 )