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