let CLSP be CollSp; :: thesis: for a, b, p, q, r being Point of CLSP st p <> q & a,b,p are_collinear & a,b,q are_collinear & p,q,r are_collinear holds
a,b,r are_collinear
let a, b, p, q, r be Point of CLSP; :: thesis: ( p <> q & a,b,p are_collinear & a,b,q are_collinear & p,q,r are_collinear implies a,b,r are_collinear )
assume that
A1: p <> q and
A2: ( a,b,p are_collinear & a,b,q are_collinear ) and
A3: p,q,r are_collinear ; :: thesis: a,b,r are_collinear

now :: thesis: ( a <> b implies a,b,r are_collinear )

assume A4: a <> b ; :: thesis: a,b,r are_collinear
then a,p,q are_collinear by A2, Th6;
then A5: p,q,a are_collinear by Th8;
a,b,b are_collinear by Th2;
then p,q,b are_collinear by A2, A4, Th3;
hence a,b,r are_collinear by A1, A3, A5, Th3; :: thesis: verum

end;

hence a,b,r are_collinear by Th2; :: thesis: verum