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