ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation F7844 on D4: Binary relation
F7844
Formulation 0
An D548: Ordered pair $(X \times Y, R)$ is a binary relation if and only if
(1) $X \times Y$ is a D191: Binary cartesian set product
(2) $R \subseteq X \times Y$ (D78: Subset)