theorem :: AFF_1:13

for AS being AffinSpace
for x, y being Element of AS st x <> y holds
ex z being Element of AS st not LIN x,y,z