Metamath Proof Explorer


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