let CS be up-3-dimensional CollProjectiveSpace; :: thesis: CS is Desarguesian
for o, a, b, c, a', b', c', r, q, p being Element of CS st o <> a' & a <> a' & o <> b' & b <> b' & o <> c' & c <> c' & not o,a,b is_collinear & not o,a,c is_collinear & not o,b,c is_collinear & a,b,p is_collinear & a',b',p is_collinear & b,c,r is_collinear & b',c',r is_collinear & a,c,q is_collinear & a',c',q is_collinear & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear holds
r,q,p is_collinear by Th26;
hence CS is Desarguesian by ANPROJ_2:def 12; :: thesis: verum