Complete the proof of **Proposition 2.35** by proving that the three remaining conditions of [Definition 2.2](https://forum.azimuthproject.org/discussion/1976) are satisfied.

**Proposition 2.35**.

Suppose \\( \mathcal{X} = (X, \le) \\) is a preorder and \\( \mathcal{X}^{op} = ( X, \ge ) \\) is its opposite.

If \\( (X, \le, I, \otimes ) \\) is a symmetric monoidal preorder then so is its opposite, \\( (X, \gt, I, \otimes ) \\) .

(i) monoidal unit : an element \\( I \in X \\)

(ii) monoidal product : a function \\( \otimes : X \times X \rightarrow X \\)

These constituents must satisfy the following properties:

**Proof** of 2.1.a

Suppose \\( x_1 \ge y_1 \\) and \\( x_2 \ge y_2 \\) in \\( \mathcal{X}^{op} \\) ;

we need to show that \\( x_1 \otimes x_2 \ge y_1 \otimes y_2 \\).

But by definition of opposite order, we have \\( y_1 \le x_1 \\)

and \\( y_2 \le x_2 \\) in \\( \mathcal{X} \\), and thus

\\( y_1 \otimes y_2 \le x_1 \otimes x_2 \\) in \\( \mathcal{X} \\).

Thus indeed \\( x_1 \otimes x_2 \ge y_1 \otimes y_2 \\) in \\( \mathcal{X}^{op} \\) .

[Previous](https://forum.azimuthproject.org/discussion/1982)

[Next](https://forum.azimuthproject.org/discussion/1984)

**Proposition 2.35**.

Suppose \\( \mathcal{X} = (X, \le) \\) is a preorder and \\( \mathcal{X}^{op} = ( X, \ge ) \\) is its opposite.

If \\( (X, \le, I, \otimes ) \\) is a symmetric monoidal preorder then so is its opposite, \\( (X, \gt, I, \otimes ) \\) .

(i) monoidal unit : an element \\( I \in X \\)

(ii) monoidal product : a function \\( \otimes : X \times X \rightarrow X \\)

These constituents must satisfy the following properties:

**Proof** of 2.1.a

Suppose \\( x_1 \ge y_1 \\) and \\( x_2 \ge y_2 \\) in \\( \mathcal{X}^{op} \\) ;

we need to show that \\( x_1 \otimes x_2 \ge y_1 \otimes y_2 \\).

But by definition of opposite order, we have \\( y_1 \le x_1 \\)

and \\( y_2 \le x_2 \\) in \\( \mathcal{X} \\), and thus

\\( y_1 \otimes y_2 \le x_1 \otimes x_2 \\) in \\( \mathcal{X} \\).

Thus indeed \\( x_1 \otimes x_2 \ge y_1 \otimes y_2 \\) in \\( \mathcal{X}^{op} \\) .

[Previous](https://forum.azimuthproject.org/discussion/1982)

[Next](https://forum.azimuthproject.org/discussion/1984)