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 A1: ( not a,b,c is_collinear & a,b,d is_collinear & c,e,d is_collinear & e <> c & 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 A1, Th4;
then ( a,d,c is_collinear & a,d,b is_collinear ) by A1, Th3;
hence contradiction by A1, Th4; :: thesis: verum