theorem Th2: :: PASCH:2

for OAS being OAffinSpace
for a, b, c, p being Element of OAS st p,b // p,c & p <> c & b <> p holds
ex d being Element of OAS st
( p,a // p,d & a,b '||' c,d & c <> d )