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