Description: PtDf is a predicate that is crucial for the definition of lines as well as proving a number of important theorems.