let PCPP be CollProjectiveSpace; :: thesis: for p, q, a, b, r being Element of PCPP 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 Element of PCPP; :: 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
( b,a,p is_collinear & b,a,q is_collinear ) by A2, Th3;
then b,p,q is_collinear by A4, Th4;
then A5: p,q,b is_collinear by Th3;
a,p,q is_collinear by A2, A4, Th4;
then p,q,a is_collinear by Th3;
hence a,b,r is_collinear by A1, A3, A5, ANPROJ_2:def 8; :: thesis: verum

end;

hence a,b,r is_collinear by ANPROJ_2:def 7; :: thesis: verum