theorem Th16: :: PASCH:16

for OAS being OAffinSpace
for a, b, c, d, p being Element of OAS st Mid p,d,a & c,d // b,a & p,c // p,b & not p,a,b are_collinear & p <> c holds
Mid p,c,b