let PCPP be CollProjectiveSpace; :: thesis: for a, b, c, d, e being Element of PCPP st not a,b,c is_collinear & a,b,d is_collinear & c,e,d is_collinear & e <> c & d <> a holds
not e,a,c is_collinear
let a, b, c, d, e be Element of PCPP; :: thesis: ( not a,b,c is_collinear & a,b,d is_collinear & c,e,d is_collinear & e <> c & d <> a implies not e,a,c is_collinear )
assume that
A1: not a,b,c is_collinear and
A2: a,b,d is_collinear and
A3: ( c,e,d is_collinear & e <> c ) and
A4: d <> a ; :: thesis: not e,a,c is_collinear
assume e,a,c is_collinear ; :: thesis: contradiction
then c,e,a is_collinear by Th3;
then c,a,d is_collinear by A3, Th4;
then A5: a,d,c is_collinear by Th3;
a,d,b is_collinear by A2, Th3;
hence contradiction by A1, A4, A5, Th4; :: thesis: verum