theorem Th18: :: PASCH:18
for OAS being OAffinSpace
for a, b, c, p being Element of OAS st p,b // p,c & b <> p holds
ex x being Element of OAS st
( p,a // p,x & b,a // c,x )