:: deftheorem defines Fanoian INCPROJ:def 12 :
for IT being IncProjStr holds
( IT is Fanoian iff for p, q, r, s, a, b, c being POINT of IT
for L, Q, R, S, A, B, C being LINE of IT st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C );