let FdSp be FanodesSp; :: thesis: for a, b, c, p, q, r being Element of FdSp st not a,b,c is_collinear & a,b '||' p,q & a,c '||' p,r & p <> q & p <> r holds
not p,q,r is_collinear
let a, b, c, p, q, r be Element of FdSp; :: thesis: ( not a,b,c is_collinear & a,b '||' p,q & a,c '||' p,r & p <> q & p <> r implies not p,q,r is_collinear )
assume that
A1: not a,b,c is_collinear and
A2: ( a,b '||' p,q & a,c '||' p,r & p <> q & p <> r ) ; :: thesis: not p,q,r is_collinear
not a,b '||' a,c by A1, Def2;
then not p,q '||' p,r by A2, PARSP_1:30;
hence not p,q,r is_collinear by Def2; :: thesis: verum