Complement of Upper Section is Lower Section
Jump to navigation
Jump to search
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
Sources
- Mizar article YELLOW_6:funcreg 7