Relation Segment is Increasing

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