let V be up-3-dimensional RealLinearSpace; :: thesis: ProjectiveSpace V is Fanoian
for p1, r2, q, r1, q1, p, r being Element of (ProjectiveSpace V) st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear by Th28;
hence ProjectiveSpace V is Fanoian by Def11; :: thesis: verum