let FdSp be FanodesSp; :: thesis: for o, a, c, b, p, q being Element of FdSp st not o,a,c is_collinear & o,a,b is_collinear & o,c,p is_collinear & o,c,q is_collinear & a,c '||' b,p & a,c '||' b,q holds
p = q
let o, a, c, b, p, q be Element of FdSp; :: thesis: ( not o,a,c is_collinear & o,a,b is_collinear & o,c,p is_collinear & o,c,q is_collinear & a,c '||' b,p & a,c '||' b,q implies p = q )
assume that
A1: ( not o,a,c is_collinear & o,a,b is_collinear ) and
A2: ( o,c,p is_collinear & o,c,q is_collinear ) and
A3: ( a,c '||' b,p & a,c '||' b,q ) ; :: thesis: p = q
A4: ( o,c '||' o,p & o,c '||' o,q ) by A2, Def2;
( not o,a '||' o,c & o,a '||' o,b ) by A1, Def2;
hence p = q by A3, A4, PARSP_1:34; :: thesis: verum