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