theorem Th16: :: PROJRED1:16

for IPP being Fanoian IncProjSp ex a, b, c, d being POINT of IPP ex A being LINE of IPP st
( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_distinct )