theorem Th1: :: PASCH:1

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