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