Binary relation

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)
Child definitions