let FdSp be FanodesSp; :: thesis: for a, b, c, d being Element of FdSp st not a,b,c is_collinear & a,b '||' c,d holds
not a,b,d is_collinear
let a, b, c, d be Element of FdSp; :: thesis: ( not a,b,c is_collinear & a,b '||' c,d implies not a,b,d is_collinear )
assume A1: ( not a,b,c is_collinear & a,b '||' c,d ) ; :: thesis: not a,b,d is_collinear

A2: now

assume a = d ; :: thesis: contradiction
then a,b '||' a,c by A1, PARSP_1:40;
hence contradiction by A1, Def2; :: thesis: verum

end;

now

assume ( c <> d & a <> d ) ; :: thesis: not a,b,d is_collinear
then ( c <> d & a <> d & not a,b,c is_collinear & a,b '||' c,d & a,c '||' c,a & c <> a & a <> b ) by A1, Th18, PARSP_1:42;
then ( not c,d,a is_collinear & d,c '||' a,b & d,a '||' a,d & a <> b & a <> d ) by Th17, PARSP_1:40, PARSP_1:42;
then ( not d,c,a is_collinear & d,c '||' a,b & d,a '||' a,d & a <> b & a <> d ) by Th15;
hence not a,b,d is_collinear by Th17; :: thesis: verum

end;

hence not a,b,d is_collinear by A1, A2; :: thesis: verum