theorem Th17: :: PARSP_2:17

for FdSp being FanodesSp
for a, b, c, d, x being Element of FdSp st not a,b,c are_collinear & a,b '||' c,d & c <> d & a,b,x are_collinear holds
not c,d,x are_collinear by Th16, PARSP_1:26;