let FdSp be FanodesSp; :: thesis: for p, q being Element of FdSp st p <> q holds
ex r being Element of FdSp st not p,q,r is_collinear
let p, q be Element of FdSp; :: thesis: ( p <> q implies ex r being Element of FdSp st not p,q,r is_collinear )
assume p <> q ; :: thesis: not for r being Element of FdSp holds p,q,r is_collinear
then consider r being Element of FdSp such that
A1: not p,q '||' p,r by Th13;
not p,q,r is_collinear by A1, Def2;
hence not for r being Element of FdSp holds p,q,r is_collinear ; :: thesis: verum