Relation Segment is Increasing
Jump to navigation
Jump to search
Theorem
Let $S$ be a set.
Let $\RR, \QQ$ be relations on $S$ such that
- $\RR \subseteq \QQ$
Let $x \in S$.
Then
- $x^\RR \subseteq x^\QQ$
where $x^\RR$ denotes the $\RR$-segment of $x$.
Proof
Let $y \in x^\RR$.
By definition of $\RR$-segment:
- $\tuple {y, x} \in \RR$
By definition of subset:
- $\tuple {y, x} \in \QQ$
Thus by definition of $\QQ$-segment:
- $y \in x^\QQ$
$\blacksquare$
Sources
- Mizar article WAYBEL_4:29