description/proof of that for linearly-ordered set, intersection of \(2\) intervals is interval as this
Topics
About: set
The table of contents of this article
Starting Context
- The reader knows a definition of linearly-ordered set.
- The reader admits the proposition that for any linearly-ordered set and any \(2\) elements, any element is larger than the 1st element and is larger than the 2nd element if and only if the element is larger than the maximum of the \(2\) elements.
- The reader admits the proposition that for any linearly-ordered set and any \(2\) elements, any element is equal to larger than the 1st element and is equal to larger than the 2nd element if and only if the element is equal to larger than the maximum of the \(2\) elements.
- The reader admits the proposition that for any linearly-ordered set and any \(2\) elements, any element is smaller than the 1st element and is smaller than the 2nd element if and only if the element is smaller than the minimum of the \(2\) elements.
- The reader admits the proposition that for any linearly-ordered set and any \(2\) elements, any element is equal to or smaller than the 1st element and is equal to or smaller than the 2nd element if and only if the element is equal to or smaller than the minimum of the \(2\) elements.
- The reader admits the proposition that for any linearly-ordered set and any \(2\) elements, any elements is larger than the 1st element and is equal to or larger than the 2nd element if and only if (the 1st elements is smaller than the 2nd element and the element is equal to or larger than the 2nd element) or (the 2nd elements is equal to or smaller than the 1st element and the element is larger than the 1st element).
- The reader admits the proposition that for any linearly-ordered set and any \(2\) elements, any elements is smaller than the 1st element and is equal to or smaller than the 2nd element if and only if (the 1st elements is equal to or smaller than the 2nd element and the element is smaller than the 1st element) or (the 2nd elements is smaller than the 1st element and the element is equal to or smaller than the 2nd element).
Target Context
- The reader will have a description and a proof of the proposition that for any linearly-ordered set, the intersection of any \(2\) intervals is an interval as this.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(S\): \(\in \{\text{ the linearly-ordered sets }\}\)
\(s_1\): \(\in S \cup \{- \infty\}\)
\(s_2\): \(\in S \cup \{\infty\}\)
\(s'_1\): \(\in S \cup \{- \infty\}\)
\(s'_2\): \(\in S \cup \{\infty\}\)
//
Statements:
\((s_1, s_2) \cap (s'_1, s'_2) = (Max (\{s_1, s'_1\}), Min (\{s_2, s'_2\})) \text{ when } Max (\{s_1, s'_1\}) \lt Min (\{s_2, s'_2\}); \emptyset \text{ when } Min (\{s_2, s'_2\}) \le Max (\{s_1, s'_1\})\)
\(\land\)
\((s_1, s_2) \cap (s'_1, s'_2] = (Max (\{s_1, s'_1\}), s_2) \text{ when } s_2 \le s'_2 \land Max (\{s_1, s'_1\}) \lt s_2; \emptyset \text{ when } s_2 \le s'_2 \land s_2 \le Max (\{s_1, s'_1\}); (Max (s_1, s'_1), s'_2] \text{ when } s'_2 \lt s_2 \land Max (s_1, s'_1) \lt s'_2; \emptyset \text{ when } s'_2 \lt s_2 \land s'_2 \le Max (s_1, s'_1)\)
\(\land\)
\((s_1, s_2) \cap [s'_1, s'_2) = [s'_1, Min (\{s_2, s'_2\}) \text{ when } s_1 \lt s'_1 \land s'_1 \lt Min (\{s_2, s'_2\}; \emptyset \text{ when } s_1 \lt s'_1 \land Min (\{s_2, s'_2\} \le s'_1; (s_1, Min (s_2, s'_2)) \text{ when } s'_1 \le s_1 \land s_1 \lt Min (s_2, s'_2); \emptyset \text{ when } s'_1 \le s_1 \land Min (s_2, s'_2) \le s_1\)
\(\land\)
\((s_1, s_2) \cap [s'_1, s'_2] = [s'_1, s_2) \text{ when } s_1 \lt s'_1 \land s_2 \le s'_2 \land s'_1 \lt s_2; \emptyset \text{ when } s_1 \lt s'_1 \land s_2 \le s'_2 \land s_2 \le s'_1; [s'_1, s'_2] \text{ when } s_1 \lt s'_1 \land s'_2 \lt s_2 \land s'_1 \le s'_2; \emptyset \text{ when } s_1 \lt s'_1 \land s'_2 \lt s_2 \land s'_2 \lt s'_1; (s_1, s_2) \text{ when } s'_1 \le s_1 \land s_2 \le s'_2 \land s_1 \lt s_2; \emptyset \text{ when } s'_1 \le s_1 \land s_2 \le s'_2 \land s_2 \le s_1; (s_1, s'_2] \text{ when } s'_1 \le s_1 \land s'_2 \lt s_2 \land s_1 \lt s'_2; \emptyset \text{ when } s'_1 \le s_1 \land s'_2 \lt s_2 \land s'_2 \le s_1\)
\(\land\)
\((s_1, s_2] \cap (s'_1, s'_2] = (Max (s_1, s'_1), Min (s_2, s'_2)] \text{ when } Max (s_1, s'_1) \lt Min (s_2, s'_2); \emptyset \text{ when } Min (s_2, s'_2) \le Max (s_1, s'_1)\)
\(\land\)
\((s_1, s_2] \cap [s'_1, s'_2) = [s'_1, s'_2) \text{ when } s_1 \lt s'_1 \land s'_2 \le s_2 \land s'_1 \lt s'_2; \emptyset \text{ when } s_1 \lt s'_1 \land s'_2 \le s_2 \land s'_2 \le s'_1; [s'_1, s_2] \text{ when } s_1 \lt s'_1 \land s_2 \lt s'_2 \land s'_1 \le s_2; \emptyset \text{ when } s_1 \lt s'_1 \land s_2 \lt s'_2 \land s_2 \lt s'_1; (s_1, s'_2) \text{ when } s'_1 \le s_1 \land s'_2 \le s_2 \land s_1 \lt s'_2; \emptyset \text{ when } s'_1 \le s_1 \land s'_2 \le s_2 \land s'_2 \le s_1; (s_1 \lt s_2] \text{ when } s'_1 \le s_1 \land s_2 \lt s'_2 \land s_1 \lt s_2; \emptyset \text{ when } s'_1 \le s_1 \land s_2 \lt s'_2 \land s_2 \le s_1\)
\(\land\)
\((s_1, s_2] \cap [s'_1, s'_2] = [s'_1, Min (s_2, s'_2)] \text{ when } s_1 \lt s'_1 \land s'_1 \le Min (s_2, s'_2); \emptyset \text{ when } s_1 \lt s'_1 \land Min (s_2, s'_2) \lt s'_1; (s_1, Min (s_2, s'_2)] \text{ when } s'_1 \le s_1 \land s_1 \lt Min (s_2, s'_2); \emptyset \text{ when } s'_1 \le s_1 \land Min (s_2, s'_2) \le s_1\)
\(\land\)
\([s_1, s_2) \cap [s'_1, s'_2) = [Max (s_1, s'_1), Min (s_2, s'_2)) \text{ when } Max (s_1, s'_1) \lt Min (s_2, s'_2); \emptyset \text{ when } Min (s_2, s'_2) \le Max (s_1, s'_1)\)
\(\land\)
\([s_1, s_2) \cap [s'_1, s'_2] = [Max (s_1, s'_1), s_2) \text{ when } s_2 \le s'_2 \land Max (s_1, s'_1) \lt s_2; \emptyset \text{ when } s_2 \le s'_2 \land s_2 \le Max (s_1, s'_1); [Max (s_1, s'_1), s'_2] \text{ when } s'_2 \lt s_2 \land Max (s_1, s'_1) \le s'_2; \emptyset \text{ when } s'_2 \lt s_2 \land s'_2 \lt Max (s_1, s'_1)\)
\(\land\)
\([s_1, s_2] \cap [s'_1, s'_2] = [Max (s_1, s'_1), Min (s_2, s'_2)] \text{ when } Max (s_1, s'_1) \le Min (s_2, s'_2); \emptyset \text{ when } Min (s_2, s'_2) \lt Max (s_1, s'_1)\)
//
\(s_1 = - \infty\) or \(s'_1 = - \infty\) with any interval lower-open-bounded means that the interval is not really lower-bounded.
\(s_2 = \infty\) or \(s'_2 = \infty\) with any interval upper-open-bounded means that the interval is not really upper-bounded.
When any interval is lower-closed-bounded, \(s_1 \in S\) or \(s'_1 \in S\), because for example, \([- \infty, s_2)\) does not make sense.
When any interval is upper-closed-bounded, \(s_2 \in S\) or \(s'_2 \in S\), because for example, \((s_1, \infty]\) does not make sense.
\(s_1 \le s_2\) and \(s'_1 \le s'_2\).
Unless the interval is both-closed-bounded, \(s_1 \lt s_2\) or \(s'_1 \lt s'_2\), because for example, \((s_1, s_1) = (s_1, s_1] = [s_1, s_1) = \emptyset\).
2: Note
In fact, there may be the notation that allows \(s_1, s_2\) or \(s'_1, s'_2\) that makes the interval empty, which we do not adapt.
The other cases like \((s_1, s_2] \cap (s'_1, s'_2)\) have not been shown, because they can be deducted from the corresponding cases like \((s_1, s_2) \cap (s'_1, s'_2]\).
3: Proof
Whole Strategy: Step 0: see that \(s_1 \lt s \land s'_1 \lt s \iff Max (\{s_1, s'_1\}) \lt s\), \(s_1 \le s \land s'_1 \le s \iff Max (\{s_1, s'_1\}) \le s\), \(s \lt s_2 \land s \lt s'_2 \iff s \lt Min (\{s_2, s'_2\})\), \(s \le s_2 \land s \le s'_2 \iff s \le Min (\{s_2, s'_2\})\), \(s_1 \lt s \land s'_1 \le s \iff (s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\), and \(s \lt s_2 \land s \le s'_2 \iff (s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\); Step 1: see the \((s_1, s_2) \cap (s'_1, s'_2)\) case; Step 2: see the \((s_1, s_2) \cap (s'_1, s'_2]\) case; Step 3: see the \((s_1, s_2) \cap [s'_1, s'_2)\) case; Step 4: see the \((s_1, s_2) \cap [s'_1, s'_2]\) case; Step 5: see the \((s_1, s_2] \cap (s'_1, s'_2]\) case; Step 6: see the \((s_1, s_2] \cap [s'_1, s'_2)\) case; Step 7: see the \((s_1, s_2] \cap [s'_1, s'_2]\) case; Step 8: see the \([s_1, s_2) \cap [s'_1, s'_2)\) case; Step 9: see the \([s_1, s_2) \cap [s'_1, s'_2]\) case; Step 10: see the \([s_1, s_2] \cap [s'_1, s'_2]\) case.
Step 0:
Let us have some definitions.
Each of \(- \infty \lt s\) and \(- \infty \le s\) means that \(s\) is not restricted by it; \(Max (\{- \infty, s\}) := s\) and \(Max (\{- \infty, - \infty\}) := - \infty\).
Each of \(s \lt \infty\) and \(s \le \infty\) means that \(s\) is not restricted by it; \(Max (\{\infty, s\}) := s\) and \(Max (\{\infty, \infty\}) := \infty\).
As some preparations, let us see some facts, which we will use frequently later.
Let \(s \in S\) be any.
\(s_1 \lt s \land s'_1 \lt s\) if and only if \(Max (\{s_1, s'_1\}) \lt s\), by the proposition that for any linearly-ordered set and any \(2\) elements, any element is larger than the 1st element and is larger than the 2nd element if and only if the element is larger than the maximum of the \(2\) elements.
\(s_1 \le s \land s'_1 \le s\) if and only if \(Max (\{s_1, s'_1\}) \le s\), by the proposition that for any linearly-ordered set and any \(2\) elements, any element is equal to larger than the 1st element and is equal to larger than the 2nd element if and only if the element is equal to larger than the maximum of the \(2\) elements.
\(s \lt s_2 \land s \lt s'_2\) if and only if \(s \lt Min (\{s_2, s'_2\})\), by the proposition that for any linearly-ordered set and any \(2\) elements, any element is smaller than the 1st element and is smaller than the 2nd element if and only if the element is smaller than the minimum of the \(2\) elements.
\(s \le s_2 \land s \le s'_2\) if and only if \(s \le Min (\{s_2, s'_2\})\), by the proposition that for any linearly-ordered set and any \(2\) elements, any element is equal to or smaller than the 1st element and is equal to or smaller than the 2nd element if and only if the element is equal to or smaller than the minimum of the \(2\) elements.
\(s_1 \lt s \land s'_1 \le s\) if and only if \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\), by the proposition that for any linearly-ordered set and any \(2\) elements, any elements is larger than the 1st element and is equal to or larger than the 2nd element if and only if (the 1st elements is smaller than the 2nd element and the element is equal to or larger than the 2nd element) or (the 2nd elements is equal to or smaller than the 1st element and the element is larger than the 1st element).
\(s \lt s_2 \land s \le s'_2\) if and only if \((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\), by the proposition that for any linearly-ordered set and any \(2\) elements, any elements is smaller than the 1st element and is equal to or smaller than the 2nd element if and only if (the 1st elements is equal to or smaller than the 2nd element and the element is smaller than the 1st element) or (the 2nd elements is smaller than the 1st element and the element is equal to or smaller than the 2nd element).
Step 1:
For each \(s \in S\), \(s \in (s_1, s_2) \cap (s'_1, s'_2)\) if and only if \(s_1 \lt s\) and \(s'_1 \lt s\) and \(s \lt s_2\) and \(s \lt s'_2\), because if \(s \in (s_1, s_2) \cap (s'_1, s'_2)\), \(s_1 \lt s\) and \(s'_1 \lt s\) and \(s \lt s_2\) and \(s \lt s'_2\); if \(s_1 \lt s\) and \(s'_1 \lt s\) and \(s \lt s_2\) and \(s \lt s'_2\), \(s \in (s_1, s_2)\) and \(s \in (s'_1, s'_2)\), so, \(s \in (s_1, s_2) \cap (s'_1, s'_2)\).
\(s_1 \lt s\) and \(s'_1 \lt s\) if and only if \(Max (s_1, s'_1) \lt s\).
\(s \lt s_2\) and \(s \lt s'_2\) if and only if \(s \lt Min (s_2, s'_2)\).
So, \(s_1 \lt s\) and \(s'_1 \lt s\) and \(s \lt s_2\) and \(s \lt s'_2\) if and only if \(Max (s_1, s'_1) \lt s\) and \(s \lt Min (s_2, s'_2)\).
\((s_1, s_2) \cap (s'_1, s'_2) = \{s \in S \vert s \in (s_1, s_2) \cap (s'_1, s'_2)\} = \{s \in S \vert Max (s_1, s'_1) \lt s \land s \lt Min (s_2, s'_2)\}\).
When \(Max (s_1, s'_1) \lt Min (s_2, s'_2)\), \(= (Max (s_1, s'_1), Min (s_2, s'_2))\).
When \(Min (s_2, s'_2) \le Max (s_1, s'_1)\), \(= \emptyset\).
Step 2:
For each \(s \in S\), \(s \in (s_1, s_2) \cap (s'_1, s'_2]\) if and only if \(s_1 \lt s\) and \(s'_1 \lt s\) and \(s \lt s_2\) and \(s \le s'_2\), because if \(s \in (s_1, s_2) \cap (s'_1, s'_2]\), \(s_1 \lt s\) and \(s'_1 \lt s\) and \(s \lt s_2\) and \(s \le s'_2\); if \(s_1 \lt s\) and \(s'_1 \lt s\) and \(s \lt s_2\) and \(s \le s'_2\), \(s \in (s_1, s_2)\) and \(s \in (s'_1, s'_2]\), so, \(s \in (s_1, s_2) \cap (s'_1, s'_2]\).
\(s_1 \lt s\) and \(s'_1 \lt s\) if and only if \(Max (s_1, s'_1) \lt s\).
\(s \lt s_2\) and \(s \le s'_2\) if and only if \((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\).
So, \(s_1 \lt s\) and \(s'_1 \lt s\) and \(s \lt s_2\) and \(s \le s'_2\) if and only if \(Max (s_1, s'_1) \lt s\) and \((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\) if and only if \(Max (s_1, s'_1) \lt s \land s_2 \le s'_2 \land s \lt s_2\) or \(Max (s_1, s'_1) \lt s \land s'_2 \lt s_2 \land s \le s'_2\) if and only if \(s_2 \le s'_2 \land Max (s_1, s'_1) \lt s \land s \lt s_2\) or \(s'_2 \lt s_2 \land Max (s_1, s'_1) \lt s \land s \le s'_2\).
\(s_2 \le s'_2\) or \(s'_2 \lt s_2\), and when \(s_2 \le s'_2\), \(s \in (s_1, s_2) \cap (s'_1, s'_2]\) if and only if \(Max (s_1, s'_1) \lt s \land s \lt s_2\); when \(s'_2 \lt s_2\), \(s \in (s_1, s_2) \cap (s'_1, s'_2]\) if and only if \(Max (s_1, s'_1) \lt s \land s \le s'_2\).
When \(s_2 \le s'_2\), \((s_1, s_2) \cap (s'_1, s'_2] = \{s \in S \vert s \in (s_1, s_2) \cap (s'_1, s'_2]\} = \{s \in S \vert Max (s_1, s'_1) \lt s \land s \lt s_2\}\).
When furthermore, \(Max (s_1, s'_1) \lt s_2\), \(= (Max (s_1, s'_1), s_2)\).
When furthermore, \(s_2 \le Max (s_1, s'_1)\), \(= \emptyset\).
When \(s'_2 \lt s_2\), \((s_1, s_2) \cap (s'_1, s'_2] = \{s \in S \vert s \in (s_1, s_2) \cap (s'_1, s'_2]\} = \{s \in S \vert Max (s_1, s'_1) \lt s \land s \le s'_2\}\).
When furthermore, \(Max (s_1, s'_1) \lt s'_2\), \(= (Max (s_1, s'_1), s'_2]\).
When furthermore, \(s'_2 \le Max (s_1, s'_1)\), \(= \emptyset\).
Step 3:
For each \(s \in S\), \(s \in (s_1, s_2) \cap [s'_1, s'_2)\) if and only if \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \lt s'_2\), because if \(s \in (s_1, s_2) \cap [s'_1, s'_2)\), \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \lt s'_2\); if \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \lt s'_2\), \(s \in (s_1, s_2)\) and \(s \in [s'_1, s'_2)\), so, \(s \in (s_1, s_2) \cap [s'_1, s'_2)\).
\(s_1 \lt s\) and \(s'_1 \le s\) if and only if \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\).
\(s \lt s_2\) and \(s \lt s'_2\) if and only if \(s \lt Min (s_2, s'_2)\).
So, \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \lt s'_2\) if and only if \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\) and \(s \lt Min (s_2, s'_2)\) if and only if \(s_1 \lt s'_1 \land s'_1 \le s \land s \lt Min (s_2, s'_2)\) or \(s'_1 \le s_1 \land s_1 \lt s \land s \lt Min (s_2, s'_2)\).
\(s_1 \lt s'_1\) or \(s'_1 \le s_1\), and when \(s_1 \lt s'_1\), \(s \in (s_1, s_2) \cap [s'_1, s'_2)\) if and only if \(s'_1 \le s \land s \lt Min (s_2, s'_2)\); when \(s'_1 \le s_1\), \(s \in (s_1, s_2) \cap [s'_1, s'_2)\) if and only if \(s_1 \lt s \land s \lt Min (s_2, s'_2)\).
When \(s_1 \lt s'_1\), \((s_1, s_2) \cap [s'_1, s'_2) = \{s \in S \vert s \in (s_1, s_2) \cap [s'_1, s'_2)\} = \{s \in S \vert s'_1 \le s \land s \lt Min (s_2, s'_2)\}\).
When furthermore, \(s'_1 \lt Min (s_2, s'_2)\), \(= [s'_1, Min (s_2, s'_2))\).
When furthermore, \(Min (s_2, s'_2) \le s'_1\), \(= \emptyset\).
When \(s'_1 \le s_1\), \((s_1, s_2) \cap [s'_1, s'_2) = \{s \in S \vert s \in (s_1, s_2) \cap [s'_1, s'_2)\} = \{s \in S \vert s_1 \lt s \land s \lt Min (s_2, s'_2)\}\).
When furthermore, \(s_1 \lt Min (s_2, s'_2)\), \(= (s_1, Min (s_2, s'_2))\).
When furthermore, \(Min (s_2, s'_2) \le s_1\), \(= \emptyset\).
Step 4:
For each \(s \in S\), \(s \in (s_1, s_2) \cap [s'_1, s'_2]\) if and only if \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \le s'_2\), because if \(s \in (s_1, s_2) \cap [s'_1, s'_2]\), \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \le s'_2\); if \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \le s'_2\), \(s \in (s_1, s_2)\) and \(s \in [s'_1, s'_2]\), so, \(s \in (s_1, s_2) \cap [s'_1, s'_2]\).
\(s_1 \lt s\) and \(s'_1 \le s\) if and only if \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\).
\(s \lt s_2\) and \(s \le s'_2\) if and only if \((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\).
So, \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \le s'_2\) if and only if \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\) and \((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\) if and only if \(s_1 \lt s'_1 \land s'_1 \le s \land s_2 \le s'_2 \land s \lt s_2\) or \(s_1 \lt s'_1 \land s'_1 \le s \land s'_2 \lt s_2 \land s \le s'_2\) or \(s'_1 \le s_1 \land s_1 \lt s \land s_2 \le s'_2 \land s \lt s_2\) or \(s'_1 \le s_1 \land s_1 \lt s \land s'_2 \lt s_2 \land s \le s'_2\) if and only if \(s_1 \lt s'_1 \land s_2 \le s'_2 \land s'_1 \le s \land s \lt s_2\) or \(s_1 \lt s'_1 \land s'_2 \lt s_2 \land s'_1 \le s \land s \le s'_2\) or \(s'_1 \le s_1 \land s_2 \le s'_2 \land s_1 \lt s \land s \lt s_2\) or \(s'_1 \le s_1 \land s'_2 \lt s_2 \land s_1 \lt s \land s \le s'_2\).
\(s_1 \lt s'_1 \land s_2 \le s'_2\) or \(s_1 \lt s'_1 \land s'_2 \lt s_2\) or \(s'_1 \le s_1 \land s_2 \le s'_2\) or \(s'_1 \le s_1 \land s'_2 \lt s_2\), and when \(s_1 \lt s'_1 \land s_2 \le s'_2\), \(s \in (s_1, s_2) \cap [s'_1, s'_2]\) if and only if \(s'_1 \le s \land s \lt s_2\); when \(s_1 \lt s'_1 \land s'_2 \lt s_2\), \(s \in (s_1, s_2) \cap [s'_1, s'_2]\) if and only if \(s'_1 \le s \land s \le s'_2\); when \(s'_1 \le s_1 \land s_2 \le s'_2\), \(s \in (s_1, s_2) \cap [s'_1, s'_2]\) if and only if \(s_1 \lt s \land s \lt s_2\); when \(s'_1 \le s_1 \land s'_2 \lt s_2\), \(s \in (s_1, s_2) \cap [s'_1, s'_2]\) if and only if \(s_1 \lt s \land s \le s'_2\).
When \(s_1 \lt s'_1 \land s_2 \le s'_2\), \((s_1, s_2) \cap [s'_1, s'_2] = \{s \in S \vert s \in (s_1, s_2) \cap [s'_1, s'_2]\} = \{s \in S \vert s'_1 \le s \land s \lt s_2\}\).
When furthermore, \(s'_1 \lt s_2\), \(= [s'_1, s_2)\).
When furthermore, \(s_2 \le s'_1\), \(= \emptyset\).
When \(s_1 \lt s'_1 \land s'_2 \lt s_2\), \((s_1, s_2) \cap [s'_1, s'_2] = \{s \in S \vert s \in (s_1, s_2) \cap [s'_1, s'_2]\} = \{s \in S \vert s'_1 \le s \land s \le s'_2\}\).
When furthermore, \(s'_1 \le s'_2\), \(= [s'_1, s'_2]\).
When furthermore, \(s'_2 \lt s'_1\), \(= \emptyset\).
When \(s'_1 \le s_1 \land s_2 \le s'_2\), \((s_1, s_2) \cap [s'_1, s'_2] = \{s \in S \vert s \in (s_1, s_2) \cap [s'_1, s'_2]\} = \{s \in S \vert s_1 \lt s \land s \lt s_2\}\).
When furthermore, \(s_1 \lt s_2\), \(= (s_1, s_2)\).
When furthermore, \(s_2 \le s_1\), \(= \emptyset\).
When \(s'_1 \le s_1 \land s'_2 \lt s_2\), \((s_1, s_2) \cap [s'_1, s'_2] = \{s \in S \vert s \in (s_1, s_2) \cap [s'_1, s'_2]\} = \{s \in S \vert s_1 \lt s \land s \le s'_2\}\).
When furthermore, \(s_1 \lt s'_2\), \(= (s_1, s'_2]\).
When furthermore, \(s'_2 \le s_1\), \(= \emptyset\).
Step 5:
For each \(s \in S\), \(s \in (s_1, s_2] \cap (s'_1, s'_2]\) if and only if \(s_1 \lt s\) and \(s'_1 \lt s\) and \(s \le s_2\) and \(s \le s'_2\), because if \(s \in (s_1, s_2] \cap (s'_1, s'_2]\), \(s_1 \lt s\) and \(s'_1 \lt s\) and \(s \le s_2\) and \(s \le s'_2\); if \(s_1 \lt s\) and \(s'_1 \lt s\) and \(s \le s_2\) and \(s \le s'_2\), \(s \in (s_1, s_2]\) and \(s \in (s'_1, s'_2]\), so, \(s \in (s_1, s_2] \cap (s'_1, s'_2]\).
\(s_1 \lt s\) and \(s'_1 \lt s\) if and only if \(Max (s_1, s'_1) \lt s\).
\(s \le s_2\) and \(s \le s'_2\) if and only if \(s \le Min (s_2, s'_2)\).
So, \(s_1 \lt s\) and \(s'_1 \lt s\) and \(s \le s_2\) and \(s \le s'_2\) if and only if \(Max (s_1, s'_1) \lt s\) and \(s \le Min (s_2, s'_2)\).
\((s_1, s_2] \cap (s'_1, s'_2] = \{s \in S \vert s \in (s_1, s_2] \cap (s'_1, s'_2]\} = \{s \in S \vert Max (s_1, s'_1) \lt s \land s \le Min (s_2, s'_2)\}\).
When \(Max (s_1, s'_1) \lt Min (s_2, s'_2)\), \(= (Max (s_1, s'_1), Min (s_2, s'_2)]\).
When \(Min (s_2, s'_2) \le Max (s_1, s'_1)\), \(= \emptyset\).
Step 6:
For each \(s \in S\), \(s \in (s_1, s_2] \cap [s'_1, s'_2)\) if and only if \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \le s_2\) and \(s \lt s'_2\), because if \(s \in (s_1, s_2] \cap [s'_1, s'_2)\), \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \le s_2\) and \(s \lt s'_2\); if \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \le s_2\) and \(s \lt s'_2\), \(s \in (s_1, s_2]\) and \(s \in [s'_1, s'_2)\), so, \(s \in (s_1, s_2] \cap [s'_1, s'_2)\).
\(s_1 \lt s\) and \(s'_1 \le s\) if and only if \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\).
\(s \le s_2\) and \(s \lt s'_2\) if and only if \((s'_2 \le s_2 \land s \lt s'_2) \lor (s_2 \lt s'_2 \land s \le s_2)\).
So, \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \le s_2\) and \(s \lt s'_2\) if and only if \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\) and \((s'_2 \le s_2 \land s \lt s'_2) \lor (s_2 \lt s'_2 \land s \le s_2)\) if and only if \(s_1 \lt s'_1 \land s'_1 \le s \land s'_2 \le s_2 \land s \lt s'_2\) or \(s_1 \lt s'_1 \land s'_1 \le s \land s_2 \lt s'_2 \land s \le s_2\) or \(s'_1 \le s_1 \land s_1 \lt s \land s'_2 \le s_2 \land s \lt s'_2\) or \(s'_1 \le s_1 \land s_1 \lt s \land s_2 \lt s'_2 \land s \le s_2\) if and only if \(s_1 \lt s'_1 \land s'_2 \le s_2 \land s'_1 \le s \land s \lt s'_2\) or \(s_1 \lt s'_1 \land s_2 \lt s'_2 \land s'_1 \le s \land s \le s_2\) or \(s'_1 \le s_1 \land s'_2 \le s_2 \land s_1 \lt s \land s \lt s'_2\) or \(s'_1 \le s_1 \land s_2 \lt s'_2 \land s_1 \lt s \land s \le s_2\).
\(s_1 \lt s'_1 \land s'_2 \le s_2\) or \(s_1 \lt s'_1 \land s_2 \lt s'_2\) or \(s'_1 \le s_1 \land s'_2 \le s_2\) or \(s'_1 \le s_1 \land s_2 \lt s'_2\), and when \(s_1 \lt s'_1 \land s'_2 \le s_2\), \(s \in (s_1, s_2] \cap [s'_1, s'_2)\) if and only if \(s'_1 \le s \land s \lt s'_2\); when \(s_1 \lt s'_1 \land s_2 \lt s'_2\), \(s \in (s_1, s_2] \cap [s'_1, s'_2)\) if and only if \(s'_1 \le s \land s \le s_2\); when \(s'_1 \le s_1 \land s'_2 \le s_2\), \(s \in (s_1, s_2] \cap [s'_1, s'_2)\) if and only if \(s_1 \lt s \land s \lt s'_2\); when \(s'_1 \le s_1 \land s_2 \lt s'_2\), \(s \in (s_1, s_2] \cap [s'_1, s'_2)\) if and only if \(s_1 \lt s \land s \le s_2\).
When \(s_1 \lt s'_1 \land s'_2 \le s_2\), \((s_1, s_2] \cap [s'_1, s'_2) = \{s \in S \vert s \in (s_1, s_2] \cap [s'_1, s'_2)\} = \{s \in S \vert s'_1 \le s \land s \lt s'_2\}\).
When furthermore, \(s'_1 \lt s'_2\), \(= [s'_1, s'_2)\).
When furthermore, \(s'_2 \le s'_1\), \(= \emptyset\).
When \(s_1 \lt s'_1 \land s_2 \lt s'_2\), \((s_1, s_2] \cap [s'_1, s'_2) = \{s \in S \vert s \in (s_1, s_2] \cap [s'_1, s'_2)\} = \{s \in S \vert s'_1 \le s \land s \le s_2\}\).
When furthermore, \(s'_1 \le s_2\), \(= [s'_1, s_2]\).
When furthermore, \(s_2 \lt s'_1\), \(= \emptyset\).
When \(s'_1 \le s_1 \land s'_2 \le s_2\), \((s_1, s_2] \cap [s'_1, s'_2) = \{s \in S \vert s \in (s_1, s_2] \cap [s'_1, s'_2)\} = \{s \in S \vert s_1 \lt s \land s \lt s'_2\}\).
When furthermore, \(s_1 \lt s'_2\), \(= (s_1, s'_2)\).
When furthermore, \(s'_2 \le s_1\), \(= \emptyset\).
When \(s'_1 \le s_1 \land s_2 \lt s'_2\), \((s_1, s_2] \cap [s'_1, s'_2) = \{s \in S \vert s \in (s_1, s_2] \cap [s'_1, s'_2)\} = \{s \in S \vert s_1 \lt s \land s \le s_2\}\).
When furthermore, \(s_1 \lt s_2\), \(= (s_1 \lt s_2]\).
When furthermore, \(s_2 \le s_1\), \(= \emptyset\).
Step 7:
For each \(s \in S\), \(s \in (s_1, s_2] \cap [s'_1, s'_2]\) if and only if \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \le s_2\) and \(s \le s'_2\), because if \(s \in (s_1, s_2] \cap [s'_1, s'_2]\), \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \le s_2\) and \(s \le s'_2\); if \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \le s_2\) and \(s \le s'_2\), \(s \in (s_1, s_2]\) and \(s \in [s'_1, s'_2]\), so, \(s \in (s_1, s_2] \cap [s'_1, s'_2]\).
\(s_1 \lt s\) and \(s'_1 \le s\) if and only if \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\).
\(s \le s_2\) and \(s \le s'_2\) if and only if \(s \le Min (s_2, s'_2)\).
So, \(s_1 \lt s\) and \(s'_1 \le s\) and \(s \le s_2\) and \(s \le s'_2\) if and only if \((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\) and \(s \le Min (s_2, s'_2)\) if and only if \(s_1 \lt s'_1 \land s'_1 \le s \land s \le Min (s_2, s'_2)\) or \(s'_1 \le s_1 \land s_1 \lt s \land s \le Min (s_2, s'_2)\).
\(s_1 \lt s'_1\) or \(s'_1 \le s_1\), and when \(s_1 \lt s'_1\), \(s \in (s_1, s_2] \cap [s'_1, s'_2]\) if and only if \(s'_1 \le s \land s \le Min (s_2, s'_2)\); when \(s'_1 \le s_1\), \(s \in (s_1, s_2] \cap [s'_1, s'_2]\) if and only if \(s_1 \lt s \land s \le Min (s_2, s'_2)\).
When \(s_1 \lt s'_1\), \((s_1, s_2] \cap [s'_1, s'_2] = \{s \in S \vert s \in (s_1, s_2] \cap [s'_1, s'_2]\} = \{s \in S \vert s'_1 \le s \land s \le Min (s_2, s'_2)\}\).
When furthermore, \(s'_1 \le Min (s_2, s'_2)\), \(= [s'_1, Min (s_2, s'_2)]\).
When furthermore, \(Min (s_2, s'_2) \lt s'_1\), \(= \emptyset\).
When \(s'_1 \le s_1\), \((s_1, s_2] \cap [s'_1, s'_2] = \{s \in S \vert s \in (s_1, s_2] \cap [s'_1, s'_2]\} = \{s \in S \vert s_1 \lt s \land s \le Min (s_2, s'_2)\}\).
When furthermore, \(s_1 \lt Min (s_2, s'_2)\), \(= (s_1, Min (s_2, s'_2)]\).
When furthermore, \(Min (s_2, s'_2) \le s_1\), \(= \emptyset\).
Step 8:
For each \(s \in S\), \(s \in [s_1, s_2) \cap [s'_1, s'_2)\) if and only if \(s_1 \le s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \lt s'_2\), because if \(s \in [s_1, s_2) \cap [s'_1, s'_2)\), \(s_1 \le s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \lt s'_2\); if \(s_1 \le s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \lt s'_2\), \(s \in [s_1, s_2)\) and \(s \in [s'_1, s'_2)\), so, \(s \in [s_1, s_2) \cap [s'_1, s'_2)\).
\(s_1 \le s\) and \(s'_1 \le s\) if and only if \(Max (s_1, s'_1) \le s\).
\(s \lt s_2\) and \(s \lt s'_2\) if and only if \(s \lt Min (s_2, s'_2)\).
So, \(s_1 \le s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \lt s'_2\) if and only if \(Max (s_1, s'_1) \lt s\) and \(s \lt Min (s_2, s'_2)\).
\([s_1, s_2) \cap [s'_1, s'_2) = \{s \in S \vert s \in [s_1, s_2) \cap [s'_1, s'_2)\} = \{s \in S \vert Max (s_1, s'_1) \le s \land s \lt Min (s_2, s'_2)\}\).
When \(Max (s_1, s'_1) \lt Min (s_2, s'_2)\), \(= [Max (s_1, s'_1), Min (s_2, s'_2))\).
When \(Min (s_2, s'_2) \le Max (s_1, s'_1)\), \(= \emptyset\).
Step 9:
For each \(s \in S\), \(s \in [s_1, s_2) \cap [s'_1, s'_2]\) if and only if \(s_1 \le s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \le s'_2\), because if \(s \in [s_1, s_2) \cap [s'_1, s'_2]\), \(s_1 \le s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \le s'_2\); if \(s_1 \le s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \le s'_2\), \(s \in [s_1, s_2)\) and \(s \in [s'_1, s'_2]\), so, \(s \in [s_1, s_2) \cap [s'_1, s'_2]\).
\(s_1 \le s\) and \(s'_1 \le s\) if and only if \(Max (s_1, s'_1) \le s\).
\(s \lt s_2\) and \(s \le s'_2\) if and only if \((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\).
So, \(s_1 \le s\) and \(s'_1 \le s\) and \(s \lt s_2\) and \(s \le s'_2\) if and only if \(Max (s_1, s'_1) \le s\) and \((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\) if and only if \(Max (s_1, s'_1) \le s \land s_2 \le s'_2 \land s \lt s_2\) or \(Max (s_1, s'_1) \le s \land s'_2 \lt s_2 \land s \le s'_2\) if and only if \(s_2 \le s'_2 \land Max (s_1, s'_1) \le s \land s \lt s_2\) or \(s'_2 \lt s_2 \land Max (s_1, s'_1) \le s \land s \le s'_2\).
\(s_2 \le s'_2\) or \(s'_2 \lt s_2\), and when \(s_2 \le s'_2\), \(s \in [s_1, s_2) \cap [s'_1, s'_2]\) if and only if \(Max (s_1, s'_1) \le s \land s \lt s_2\); when \(s'_2 \lt s_2\), \(s \in [s_1, s_2) \cap [s'_1, s'_2]\) if and only if \(Max (s_1, s'_1) \le s \land s \le s'_2\).
When \(s_2 \le s'_2\), \([s_1, s_2) \cap [s'_1, s'_2] = \{s \in S \vert s \in [s_1, s_2) \cap [s'_1, s'_2]\} = \{s \in S \vert Max (s_1, s'_1) \le s \land s \lt s_2\}\).
When furthermore, \(Max (s_1, s'_1) \lt s_2\), \(= [Max (s_1, s'_1), s_2)\).
When furthermore, \(s_2 \le Max (s_1, s'_1)\), \(= \emptyset\).
When \(s'_2 \lt s_2\), \([s_1, s_2) \cap [s'_1, s'_2] = \{s \in S \vert s \in [s_1, s_2) \cap [s'_1, s'_2]\} = \{s \in S \vert Max (s_1, s'_1) \le s \land s \le s'_2\}\).
When furthermore, \(Max (s_1, s'_1) \le s'_2\), \(= [Max (s_1, s'_1) \le s'_2]\).
When furthermore, \(s'_2 \lt Max (s_1, s'_1)\), \(= \emptyset\).
Step 10:
For each \(s \in S\), \(s \in [s_1, s_2] \cap [s'_1, s'_2]\) if and only if \(s_1 \le s\) and \(s'_1 \le s\) and \(s \le s_2\) and \(s \le s'_2\), because if \(s \in [s_1, s_2] \cap [s'_1, s'_2]\), \(s_1 \le s\) and \(s'_1 \le s\) and \(s \le s_2\) and \(s \le s'_2\); if \(s_1 \le s\) and \(s'_1 \le s\) and \(s \le s_2\) and \(s \le s'_2\), \(s \in [s_1, s_2]\) and \(s \in [s'_1, s'_2]\), so, \(s \in [s_1, s_2] \cap [s'_1, s'_2]\).
\(s_1 \le s\) and \(s'_1 \le s\) if and only if \(Max (s_1, s'_1) \le s\).
\(s \le s_2\) and \(s \le s'_2\) if and only if \(s \le Min (s_2, s'_2)\).
So, \(s_1 \le s\) and \(s'_1 \le s\) and \(s \le s_2\) and \(s \le s'_2\) if and only if \(Max (s_1, s'_1) \le s\) and \(s \le Min (s_2, s'_2)\).
\([s_1, s_2] \cap [s'_1, s'_2] = \{s \in S \vert s \in [s_1, s_2] \cap [s'_1, s'_2]\} = \{s \in S \vert Max (s_1, s'_1) \le s \land s \le Min (s_2, s'_2)\}\).
When \(Max (s_1, s'_1) \le Min (s_2, s'_2)\), \(= [Max (s_1, s'_1), Min (s_2, s'_2)]\).
When \(Min (s_2, s'_2) \lt Max (s_1, s'_1)\), \(= \emptyset\).
