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