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