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 are_collinear & not o,a,c are_collinear & not o,b,c are_collinear & a,b,p are_collinear & a9,b9,p are_collinear & b,c,r are_collinear & b9,c9,r are_collinear & a,c,q are_collinear & a9,c9,q are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear holds
r,q,p are_collinear by Th21;
hence CS is Desarguesian by ANPROJ_2:def 12; :: thesis: verum