**ordered set**if and only if

(1) | $X$ is a D11: Set |

(2) | ${\preceq}$ is an D378: Ordering relation on $X$ |

Definition D1707

Ordered set

Formulation 0

An D548: Ordered pair $P = (X, {\preceq})$ is an **ordered set** if and only if

(1) | $X$ is a D11: Set |

(2) | ${\preceq}$ is an D378: Ordering relation on $X$ |

Children

▶ | D714: Dedekind cut |