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