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	$$classPtDf\left(A,B\right)$$