Complement of Upper Section is Lower Section

Theorem

Let $\struct {S, \preceq}$ be an ordered set.

Let $L$ be an upper section.

Then $S \setminus L$ is a lower section.

Proof

This follows mutatis mutandis from the proof of Complement of Lower Section is Upper Section.

$\blacksquare$

Also see

• Complement of Lower Section is Upper Section

Sources

• Mizar article YELLOW_6:funcreg 7