let CLSP be CollSp; :: thesis: for a, b, p, q, r being Point of CLSP st a <> b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear holds
p,q,r is_collinear
let a, b, p, q, r be Point of CLSP; :: thesis: ( a <> b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear implies p,q,r is_collinear )
assume that
A1: a <> b and
A2: ( a,b,p is_collinear & a,b,q is_collinear ) and
A3: a,b,r is_collinear ; :: thesis: p,q,r is_collinear
A4: [a,b,r] in the Collinearity of CLSP by A3, Def2;
( [a,b,p] in the Collinearity of CLSP & [a,b,q] in the Collinearity of CLSP ) by A2, Def2;
then [p,q,r] in the Collinearity of CLSP by A1, A4, Def4;
hence p,q,r is_collinear by Def2; :: thesis: verum