theorem :: PARSP_2:19

for FdSp being FanodesSp
for a, b, p, q, o being Element of FdSp st o <> a & o <> b & o,a,b are_collinear & o,a,p are_collinear & o,b,q are_collinear holds
a,b '||' p,q