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

now

assume A4: a <> b ; :: thesis: a,b,r is_collinear
then a,p,q is_collinear by A2, Th11;
then A5: p,q,a is_collinear by Th13;
a,b,b is_collinear by Th7;
then p,q,b is_collinear by A2, A4, Th8;
hence a,b,r is_collinear by A1, A3, A5, Th8; :: thesis: verum

end;

hence a,b,r is_collinear by Th7; :: thesis: verum