let FdSp be FanodesSp; :: thesis: for a, b, c, d, p, q being Element of FdSp st not a,b '||' c,d & a,b,p are_collinear & a,b,q are_collinear & c,d,p are_collinear & c,d,q are_collinear holds
p = q
let a, b, c, d, p, q be Element of FdSp; :: thesis: ( not a,b '||' c,d & a,b,p are_collinear & a,b,q are_collinear & c,d,p are_collinear & c,d,q are_collinear implies p = q )
assume that
A1: not a,b '||' c,d and
A2: ( a,b,p are_collinear & a,b,q are_collinear ) and
A3: ( c,d,p are_collinear & c,d,q are_collinear ) ; :: thesis: p = q
c,d '||' p,q by A3, Th15;
then A4: p,q '||' c,d by PARSP_1:23;
a,b '||' p,q by A2, Th15;
then p,q '||' a,b by PARSP_1:23;
hence p = q by A1, A4, PARSP_1:def 12; :: thesis: verum