theorem :: PASCH:13

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