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