# Definition:Ordered Subset

Jump to navigation
Jump to search

## Definition

Let $R = \struct{S, \preceq}$ be a relational structure.

A **ordered subset** of $R$ is a relational structure $\struct{S', \preceq'}$ such that

- $S'$ is a subset of $S$,
- $\mathord\preceq' = \mathord\preceq \cap \paren{S' \times S'}$

That is

- $\forall x, y \in S': x \preceq y \iff x \preceq' y$

## Sources

- Mizar article YELLOW_0:def 13

- Mizar article YELLOW_0:def 14