for FCPS being up-3-dimensional CollProjectiveSpace
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