Syntax definition cptdfc

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

	Ref	Expression
Assertion	cptdfc	class PtDf ( A , B )