theorem :: AFF_1:56

for AS being AffinSpace
for a, a9, b, b9, o, x being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & LIN o,b,x & a,b // a9,b9 & a,b // a9,x holds
b9 = x