theorem Th8: :: PASCH:8
for OAS being OAffinSpace
for a, b, c, d, p being Element of OAS st Mid p,b,c & p,a,d are_collinear & a,b '||' c,d & not p,a,b are_collinear holds
Mid p,a,d