theorem Th4: :: PASCH:4

for OAS being OAffinSpace
for a, b, c, d1, d2, p being Element of OAS st not p,a,b are_collinear & p,b,c are_collinear & p,a,d1 are_collinear & p,a,d2 are_collinear & a,b '||' c,d1 & a,b '||' c,d2 holds
d1 = d2