# Ordering

## Definition

A binary relation \(\mathrel{R}\), on a set \(S\), is an ordering if and only if:

- \(\mathrel{R}\) is reflexive:
- \(\forall x \in S : x{\mathrel{R}}x\)
- \(\mathrel{R}\) is transitive:
- \(\forall x,y,z \in S : x{\mathrel{R}}y \wedge y{\mathrel{R}}z \Rightarrow x{\mathrel{R}}z\)
- \(\mathrel{R}\) is anti-symmetric:
- \(\forall x,y \in S : x{\mathrel{R}}y \wedge y{\mathrel{R}}x \Rightarrow x = y\)

## Axioms

```
order_refl: ?x ≤ ?x
order_trans: ?x ≤ ?y \(\Longrightarrow\) ?y ≤ ?z
order_antisym: ?x ≤ ?y \(\Longrightarrow\) ?y ≤ ?x \(\Longrightarrow\) ?x = ?y
```

**THEOREM**
\(x \le x \sqcup y\)

```
sup_ge1: ?x ≤ ?x \(\sqcup\) ?y
```

Proof unavailable

**THEOREM**
\(y \le x \sqcup y\)

```
sup_ge2: ?y ≤ ?x \(\sqcup\) ?y
```

Proof unavailable

**THEOREM**
A non-empty subset of an ordered set has one supremum at most.

Proof available

**THEOREM**
A non-empty subset of an ordered set has one infimum at most.

Proof available

**THEOREM**
An ordered set has one greatest element at most.

Proof available

**THEOREM**
An ordered set has one smallest element at most.

Proof available

## Proper supersets