**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) |

▼ | Set of symbols |

▼ | Alphabet |

▼ | Deduction system |

▼ | Theory |

▼ | Zermelo-Fraenkel set theory |

▼ | Set |

▼ | Binary cartesian set product |

Definition D4

Binary relation

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

Children