let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, a9, d, d9, o, s being Element of FCPS st not o,a,d are_collinear & o,d,d9 are_collinear & d <> d9 & a9,d9,s are_collinear & o,a,a9 are_collinear & o <> a9 holds
s <> d
let a, a9, d, d9, o, s be Element of FCPS; :: thesis: ( not o,a,d are_collinear & o,d,d9 are_collinear & d <> d9 & a9,d9,s are_collinear & o,a,a9 are_collinear & o <> a9 implies s <> d )
assume that
A1: not o,a,d are_collinear and
A2: o,d,d9 are_collinear and
A3: d <> d9 and
A4: a9,d9,s are_collinear and
A5: o,a,a9 are_collinear and
A6: o <> a9 ; :: thesis: s <> d
assume not s <> d ; :: thesis: contradiction
then A7: d,d9,a9 are_collinear by A4, Th1;
d,d9,o are_collinear by A2, Th1;
then d,o,a9 are_collinear by A3, A7, COLLSP:6;
then A8: o,a9,d are_collinear by Th1;
o,a9,a are_collinear by A5, Th1;
hence contradiction by A1, A6, A8, COLLSP:6; :: thesis: verum