theorem :: PASCH:12

for OAS being OAffinSpace
for a, a9, b, b9, p being Element of OAS st not p,a,b are_collinear & a,p // p,a9 & b,p // p,b9 & a,b '||' a9,b9 holds
a,b // b9,a9