theorem Th15: :: PASCH:15

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