let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for o, a, d, d', s, a' being Element of FCPS st not o,a,d is_collinear & o,d,d' is_collinear & a,d,s is_collinear & d <> d' & a',d',s is_collinear & o,a,a' is_collinear & o <> a' holds
s <> d
let o, a, d, d', s, a' be Element of FCPS; :: thesis: ( not o,a,d is_collinear & o,d,d' is_collinear & a,d,s is_collinear & d <> d' & a',d',s is_collinear & o,a,a' is_collinear & o <> a' implies s <> d )
assume A1: ( not o,a,d is_collinear & o,d,d' is_collinear & a,d,s is_collinear & d <> d' & a',d',s is_collinear & o,a,a' is_collinear & o <> a' ) ; :: thesis: s <> d
assume not s <> d ; :: thesis: contradiction
then A2: d,d',a' is_collinear by A1, Th1;
d,d',o is_collinear by A1, Th1;
then d,o,a' is_collinear by A1, A2, COLLSP:11;
then A3: o,a',d is_collinear by Th1;
o,a',a is_collinear by A1, Th1;
hence contradiction by A1, A3, COLLSP:11; :: thesis: verum