theorem :: PROJRED1:15

for IPP being Fanoian IncProjSp ex a being POINT of IPP ex A, B, C, D being LINE of IPP st
( a on A & a on B & a on C & a on D & A,B,C,D are_mutually_distinct )