リニアリーオーダードセット（線形順序集合）に対して、\(2\)個のインターバル（区間）たちのインターセクション（共通集合）はインターバル（区間）である、このように、ことの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、リニアリーオーダードセット（線形順序集合）の定義を知っている。
- 読者は、任意のリニアリーオーダードセット（線形順序集合）および任意の\(2\)個の要素たちに対して、任意の要素は第1要素より大きく第2要素より大きい、もしも、当該要素は\(2\)個の要素たちのマキシマム（最大）より大きい場合、そしてその場合に限って、という命題を認めている。
- 読者は、任意のリニアリーオーダードセット（線形順序集合）および任意の\(2\)個の要素たちに対して、任意の要素は第1要素以上で第2要素以上である、もしも、当該要素は\(2\)個の要素たちのマキシマム（最大）以上である場合、そしてその場合に限って、という命題を認めている。
- 読者は、任意のリニアリーオーダードセット（線形順序集合）および任意の\(2\)個の要素たちに対して、任意の要素は第1要素より小さく第2要素より小さい、もしも、当該要素は\(2\)個の要素たちのミニマム（最小）より小さい場合、そしてその場合に限って、という命題を認めている。
- 読者は、任意のリニアリーオーダードセット（線形順序集合）および任意の\(2\)個の要素たちに対して、任意の要素は第1要素以下で第2要素以下である、もしも、当該要素は\(2\)個の要素たちのミニマム（最小）以下である場合、そしてその場合に限って、という命題を認めている。
- 読者は、任意のリニアリーオーダードセット（線形順序集合）および任意の\(2\)個の要素たちに対して、任意の要素は第1要素より大きく第2要素以上である、もしも、（第1要素は第2要素より小さく当該要素は第2要素以上である）または（第2要素は第1要素以下であり当該要素は第1要素より大きい)である場合、そして、その場合に限って、という命題を認めている。
- 読者は、任意のリニアリーオーダードセット（線形順序集合）および任意の\(2\)個の要素たちに対して、任意の要素は第1要素より小さく第2要素以下である、もしも、（第1要素は第2要素以下であり当該要素は第2要素より小さい）または（第2要素は第1要素より小さく当該要素は第2要素以下である)である場合、そして、その場合に限って、という命題を認めている。
ターゲットコンテキスト
- 読者は、任意のリニアリーオーダードセット（線形順序集合）に対して、任意の\(2\)個のインターバル（区間）たちのインターセクション（共通集合）はあるインターバル（区間）である、このように、という命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S\): \(\in \{\text{ 全てのリニアリーオーダードセット（線形順序集合）たち }\}\)
\(s_1\): \(\in S \cup \{- \infty\}\)
\(s_2\): \(\in S \cup \{\infty\}\)
\(s'_1\): \(\in S \cup \{- \infty\}\)
\(s'_2\): \(\in S \cup \{\infty\}\)
//
ステートメント（言明）たち:
\((s_1, s_2) \cap (s'_1, s'_2) = (Max (\{s_1, s'_1\}), Min (\{s_2, s'_2\})) \text{ 、 } Max (\{s_1, s'_1\}) \lt Min (\{s_2, s'_2\}) \text{ である時 }; \emptyset \text{ 、 } Min (\{s_2, s'_2\}) \le Max (\{s_1, s'_1\}) \text{ である時 }\)
\(\land\)
\((s_1, s_2) \cap (s'_1, s'_2] = (Max (\{s_1, s'_1\}), s_2) \text{ 、 } s_2 \le s'_2 \land Max (\{s_1, s'_1\}) \lt s_2 \text{ である時 }; \emptyset \text{ 、 } s_2 \le s'_2 \land s_2 \le Max (\{s_1, s'_1\}) \text{ である時 }; (Max (s_1, s'_1), s'_2] \text{ 、 } s'_2 \lt s_2 \land Max (s_1, s'_1) \lt s'_2 \text{ である時 }; \emptyset \text{ 、 } s'_2 \lt s_2 \land s'_2 \le Max (s_1, s'_1) \text{ である時 }\)
\(\land\)
\((s_1, s_2) \cap [s'_1, s'_2) = [s'_1, Min (\{s_2, s'_2\}) \text{ 、 } s_1 \lt s'_1 \land s'_1 \lt Min (\{s_2, s'_2\} \text{ である時 }; \emptyset \text{ 、 } s_1 \lt s'_1 \land Min (\{s_2, s'_2\} \le s'_1 \text{ である時 }; (s_1, Min (s_2, s'_2)) \text{ 、 } s'_1 \le s_1 \land s_1 \lt Min (s_2, s'_2) \text{ である時 }; \emptyset \text{ 、 } s'_1 \le s_1 \land Min (s_2, s'_2) \le s_1 \text{ である時 }\)
\(\land\)
\((s_1, s_2) \cap [s'_1, s'_2] = [s'_1, s_2) \text{ 、 } s_1 \lt s'_1 \land s_2 \le s'_2 \land s'_1 \lt s_2 \text{ である時 }; \emptyset \text{ 、 } s_1 \lt s'_1 \land s_2 \le s'_2 \land s_2 \le s'_1 \text{ である時 }; [s'_1, s'_2] \text{ 、 } s_1 \lt s'_1 \land s'_2 \lt s_2 \land s'_1 \le s'_2 \text{ である時 }; \emptyset \text{ 、 } s_1 \lt s'_1 \land s'_2 \lt s_2 \land s'_2 \lt s'_1 \text{ である時 }; (s_1, s_2) \text{ 、 } s'_1 \le s_1 \land s_2 \le s'_2 \land s_1 \lt s_2 \text{ である時 }; \emptyset \text{ 、 } s'_1 \le s_1 \land s_2 \le s'_2 \land s_2 \le s_1 \text{ である時 }; (s_1, s'_2] \text{ 、 } s'_1 \le s_1 \land s'_2 \lt s_2 \land s_1 \lt s'_2 \text{ である時 }; \emptyset \text{ 、 } s'_1 \le s_1 \land s'_2 \lt s_2 \land s'_2 \le s_1 \text{ である時 }\)
\(\land\)
\((s_1, s_2] \cap (s'_1, s'_2] = (Max (s_1, s'_1), Min (s_2, s'_2)] \text{ 、 } Max (s_1, s'_1) \lt Min (s_2, s'_2) \text{ である時 }; \emptyset \text{ 、 } Min (s_2, s'_2) \le Max (s_1, s'_1) \text{ である時 }\)
\(\land\)
\((s_1, s_2] \cap [s'_1, s'_2) = [s'_1, s'_2) \text{ 、 } s_1 \lt s'_1 \land s'_2 \le s_2 \land s'_1 \lt s'_2 \text{ である時 }; \emptyset \text{ 、 } s_1 \lt s'_1 \land s'_2 \le s_2 \land s'_2 \le s'_1 \text{ である時 }; [s'_1, s_2] \text{ 、 } s_1 \lt s'_1 \land s_2 \lt s'_2 \land s'_1 \le s_2 \text{ である時 }; \emptyset \text{ 、 } s_1 \lt s'_1 \land s_2 \lt s'_2 \land s_2 \lt s'_1 \text{ である時 }; (s_1, s'_2) \text{ 、 } s'_1 \le s_1 \land s'_2 \le s_2 \land s_1 \lt s'_2 \text{ である時 }; \emptyset \text{ 、 } s'_1 \le s_1 \land s'_2 \le s_2 \land s'_2 \le s_1 \text{ である時 }; (s_1 \lt s_2] \text{ 、 } s'_1 \le s_1 \land s_2 \lt s'_2 \land s_1 \lt s_2 \text{ である時 }; \emptyset \text{ 、 } s'_1 \le s_1 \land s_2 \lt s'_2 \land s_2 \le s_1 \text{ である時 }\)
\(\land\)
\((s_1, s_2] \cap [s'_1, s'_2] = [s'_1, Min (s_2, s'_2)] \text{ 、 } s_1 \lt s'_1 \land s'_1 \le Min (s_2, s'_2) \text{ である時 }; \emptyset \text{ 、 } s_1 \lt s'_1 \land Min (s_2, s'_2) \lt s'_1 \text{ である時 }; (s_1, Min (s_2, s'_2)] \text{ 、 } s'_1 \le s_1 \land s_1 \lt Min (s_2, s'_2) \text{ である時 }; \emptyset \text{ 、 } s'_1 \le s_1 \land Min (s_2, s'_2) \le s_1 \text{ である時 }\)
\(\land\)
\([s_1, s_2) \cap [s'_1, s'_2) = [Max (s_1, s'_1), Min (s_2, s'_2)) \text{ 、 } Max (s_1, s'_1) \lt Min (s_2, s'_2) \text{ である時 }; \emptyset \text{ 、 } Min (s_2, s'_2) \le Max (s_1, s'_1) \text{ である時 }\)
\(\land\)
\([s_1, s_2) \cap [s'_1, s'_2] = [Max (s_1, s'_1), s_2) \text{ 、 } s_2 \le s'_2 \land Max (s_1, s'_1) \lt s_2 \text{ である時 }; \emptyset \text{ 、 } s_2 \le s'_2 \land s_2 \le Max (s_1, s'_1) \text{ である時 }; [Max (s_1, s'_1), s'_2] \text{ 、 } s'_2 \lt s_2 \land Max (s_1, s'_1) \le s'_2 \text{ である時 }; \emptyset \text{ 、 } s'_2 \lt s_2 \land s'_2 \lt Max (s_1, s'_1) \text{ である時 }\)
\(\land\)
\([s_1, s_2] \cap [s'_1, s'_2] = [Max (s_1, s'_1), Min (s_2, s'_2)] \text{ 、 } Max (s_1, s'_1) \le Min (s_2, s'_2) \text{ である時 }; \emptyset \text{ 、 } Min (s_2, s'_2) \lt Max (s_1, s'_1) \text{ である時 }\)
//
\(s_1 = - \infty\)または\(s'_1 = - \infty\)であるローワーオープンバウンデッド（下方開有界）任意のインターバル（区間）は、当該インターバル（区間）は本当にはローワーバウンデッド（下方有界）でないことを意味する。
\(s_2 = \infty\)または\(s'_2 = \infty\)であるアッパーオープンバウンデッド（上方開有界）任意のインターバル（区間）は、当該インターバル（空間）は本当にはアッパーバウンデッド（上方有界）でないことを意味する。
任意のインターバル（区間）がローワークローズドバウンデッド（下方閉有界）である時、\(s_1 \in S\)または\(s'_1 \in S\)、なぜなら、例えば、\([- \infty, s_2)\)は意味をなさない。
任意のインターバル（区間）がアッパークローズドバウンデッド（上方閉有界）である時、\(s_2 \in S\)または\(s'_2 \in S\)、なぜなら、例えば、\((s_1, \infty]\)は意味をなさない。
\(s_1 \le s_2\)および\(s'_1 \le s'_2\)。
当該インターバル（区間）が両方クローズドバウンデッド（閉有界）でない場合、\(s_1 \lt s_2\)または\(s'_1 \lt s'_2\)、なぜなら、例えば、\((s_1, s_1) = (s_1, s_1] = [s_1, s_1) = \emptyset\)。
2: 注
実のところ、当該インターバル（区間）を空にする\(s_1, s_2\)または\(s'_1, s'_2\)を許す記法もあるかもしれない、それを、私たちは採択しない。
\((s_1, s_2] \cap (s'_1, s'_2)\)のような他のケースたちは示されていない、なぜなら、それらは、\((s_1, s_2) \cap (s'_1, s'_2]\)のような対応するケースたちから導出できる。
3: 証明
全体戦略: ステップ0: \(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)\)、\(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)\)であることを見る; ステップ1: \((s_1, s_2) \cap (s'_1, s'_2)\)ケースを見る; ステップ2: \((s_1, s_2) \cap (s'_1, s'_2]\)ケースを見る; ステップ3: \((s_1, s_2) \cap [s'_1, s'_2)\)ケースを見る; ステップ4: \((s_1, s_2) \cap [s'_1, s'_2]\)ケースを見る; ステップ5: \((s_1, s_2] \cap (s'_1, s'_2]\)ケースを見る; ステップ6: \((s_1, s_2] \cap [s'_1, s'_2)\)ケースを見る; ステップ7: \((s_1, s_2] \cap [s'_1, s'_2]\)ケースを見る; ステップ8: \([s_1, s_2) \cap [s'_1, s'_2)\)ケースを見る; ステップ9: \([s_1, s_2) \cap [s'_1, s'_2]\)ケースを見る; ステップ10: \([s_1, s_2] \cap [s'_1, s'_2]\)ケースを見る。
ステップ0:
いくつかの定義たちを得よう。
\(- \infty \lt s\)および\(- \infty \le s\)の各々は、\(s\)はそれによって制限されないことを意味する; \(Max (\{- \infty, s\}) := s\)および\(Max (\{- \infty, - \infty\}) := - \infty\)。
\(s \lt \infty\)および\(s \le \infty\)の各々は、\(s\)はそれによって制限されないことを意味する; \(Max (\{\infty, s\}) := s\)および\(Max (\{\infty, \infty\}) := \infty\)。
準備として、いくつかの事実たちを見よう、それらを私たちは、以降に、頻繁に使う。
\(s \in S\)を任意のものとしよう。
\(s_1 \lt s \land s'_1 \lt s\)、もしも、\(Max (\{s_1, s'_1\}) \lt s\)である場合、そしてその場合に限って、任意のリニアリーオーダードセット（線形順序集合）および任意の\(2\)個の要素たちに対して、任意の要素は第1要素より大きく第2要素より大きい、もしも、当該要素は\(2\)個の要素たちのマキシマム（最大）より大きい場合、そしてその場合に限って、という命題によって。
\(s_1 \le s \land s'_1 \le s\)、もしも、\(Max (\{s_1, s'_1\}) \le s\)である場合、そしてその場合に限って、任意のリニアリーオーダードセット（線形順序集合）および任意の\(2\)個の要素たちに対して、任意の要素は第1要素以上で第2要素以上である、もしも、当該要素は\(2\)個の要素たちのマキシマム（最大）以上である場合、そしてその場合に限って、という命題によって。
\(s \lt s_2 \land s \lt s'_2\)、もしも、\(s \lt Min (\{s_2, s'_2\})\)である場合、そしてその場合に限って、任意のリニアリーオーダードセット（線形順序集合）および任意の\(2\)個の要素たちに対して、任意の要素は第1要素より小さく第2要素より小さい、もしも、当該要素は\(2\)個の要素たちのミニマム（最小）より小さい場合、そしてその場合に限って、という命題によって。
\(s \le s_2 \land s \le s'_2\)、もしも、\(s \le Min (\{s_2, s'_2\})\)である場合、そしてその場合に限って、任意のリニアリーオーダードセット（線形順序集合）および任意の\(2\)個の要素たちに対して、任意の要素は第1要素以下で第2要素以下である、もしも、当該要素は\(2\)個の要素たちのミニマム（最小）以下である場合、そしてその場合に限って、という命題によって。
\(s_1 \lt s \land s'_1 \le s\)、もしも、\((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\)である場合、そしてその場合に限って、任意のリニアリーオーダードセット（線形順序集合）および任意の\(2\)個の要素たちに対して、任意の要素は第1要素より大きく第2要素以上である、もしも、（第1要素は第2要素より小さく当該要素は第2要素以上である）または（第2要素は第1要素以下であり当該要素は第1要素より大きい)である場合、そして、その場合に限って、という命題によって。
\(s \lt s_2 \land s \le s'_2\)、もしも、\((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\)である場合、そしてその場合に限って、任意のリニアリーオーダードセット（線形順序集合）および任意の\(2\)個の要素たちに対して、任意の要素は第1要素より小さく第2要素以下である、もしも、（第1要素は第2要素以下であり当該要素は第2要素より小さい）または（第2要素は第1要素より小さく当該要素は第2要素以下である)である場合、そして、その場合に限って、という命題によって。
ステップ1:
各\(s \in S\)に対して、\(s \in (s_1, s_2) \cap (s'_1, s'_2)\)、もしも、\(s_1 \lt s\)および\(s'_1 \lt s\)および\(s \lt s_2\)および\(s \lt s'_2\)である場合、そしてその場合に限って、なぜなら、もしも、\(s \in (s_1, s_2) \cap (s'_1, s'_2)\)である場合、\(s_1 \lt s\)および\(s'_1 \lt s\)および\(s \lt s_2\)および\(s \lt s'_2\); もしも、\(s_1 \lt s\)および\(s'_1 \lt s\)および\(s \lt s_2\)および\(s \lt s'_2\)である場合、\(s \in (s_1, s_2)\)および\(s \in (s'_1, s'_2)\)、したがって、\(s \in (s_1, s_2) \cap (s'_1, s'_2)\)。
\(s_1 \lt s\)および\(s'_1 \lt s\)、もしも、\(Max (s_1, s'_1) \lt s\)である場合、そしてその場合に限って。
\(s \lt s_2\)および\(s \lt s'_2\)、もしも、\(s \lt Min (s_2, s'_2)\)である場合、そしてその場合に限って。
したがって、\(s_1 \lt s\)および\(s'_1 \lt s\)および\(s \lt s_2\)および\(s \lt s'_2\)、もしも、\(Max (s_1, s'_1) \lt s\)および\(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)\}\)。
\(Max (s_1, s'_1) \lt Min (s_2, s'_2)\)である時は、\(= (Max (s_1, s'_1), Min (s_2, s'_2))\)。
\(Min (s_2, s'_2) \le Max (s_1, s'_1)\)である時は、\(= \emptyset\)。
ステップ2:
各\(s \in S\)に対して、\(s \in (s_1, s_2) \cap (s'_1, s'_2]\)、もしも、\(s_1 \lt s\)および\(s'_1 \lt s\)および\(s \lt s_2\)および\(s \le s'_2\)である場合、そしてその場合に限って、なぜなら、もしも、\(s \in (s_1, s_2) \cap (s'_1, s'_2]\)である場合、\(s_1 \lt s\)および\(s'_1 \lt s\)および\(s \lt s_2\)および\(s \le s'_2\); もしも、\(s_1 \lt s\)および\(s'_1 \lt s\)および\(s \lt s_2\)および\(s \le s'_2\)である場合、\(s \in (s_1, s_2)\)および\(s \in (s'_1, s'_2]\)、したがって、\(s \in (s_1, s_2) \cap (s'_1, s'_2]\)。
\(s_1 \lt s\)および\(s'_1 \lt s\)、もしも、\(Max (s_1, s'_1) \lt s\)である場合、そしてその場合に限って。
\(s \lt s_2\)および\(s \le s'_2\)、もしも、\((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\)である場合、そしてその場合に限って。
したがって、\(s_1 \lt s\)および\(s'_1 \lt s\)および\(s \lt s_2\)および\(s \le s'_2\)、もしも、\(Max (s_1, s'_1) \lt s\)および\((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\)である場合、そしてその場合に限って、もしも、\(Max (s_1, s'_1) \lt s \land s_2 \le s'_2 \land s \lt s_2\)または\(Max (s_1, s'_1) \lt s \land s'_2 \lt s_2 \land s \le s'_2\)である場合、そしてその場合に限って、もしも、\(s_2 \le s'_2 \land Max (s_1, s'_1) \lt s \land s \lt s_2\)または\(s'_2 \lt s_2 \land Max (s_1, s'_1) \lt s \land s \le s'_2\)である場合、そしてその場合に限って。
\(s_2 \le s'_2\)または\(s'_2 \lt s_2\)、そして、\(s_2 \le s'_2\)である時は、\(s \in (s_1, s_2) \cap (s'_1, s'_2]\)、もしも、\(Max (s_1, s'_1) \lt s \land s \lt s_2\)である場合、そしてその場合に限って; \(s'_2 \lt s_2\)である時は、\(s \in (s_1, s_2) \cap (s'_1, s'_2]\)、もしも、\(Max (s_1, s'_1) \lt s \land s \le s'_2\)である場合、そしてその場合に限って。
\(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\}\)。
その上\(Max (s_1, s'_1) \lt s_2\)である時は、\(= (Max (s_1, s'_1), s_2)\)。
その上\(s_2 \le Max (s_1, s'_1)\)である時は、\(= \emptyset\)。
\(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\}\)。
その上\(Max (s_1, s'_1) \lt s'_2\)である時は、\(= (Max (s_1, s'_1), s'_2]\)。
その上\(s'_2 \le Max (s_1, s'_1)\)である時は、\(= \emptyset\)。
ステップ3:
各\(s \in S\)に対して、\(s \in (s_1, s_2) \cap [s'_1, s'_2)\)、もしも、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \lt s'_2\)である場合、そしてその場合に限って、なぜなら、もしも、\(s \in (s_1, s_2) \cap [s'_1, s'_2)\)である場合、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \lt s'_2\); もしも、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \lt s'_2\)である場合、\(s \in (s_1, s_2)\)および\(s \in [s'_1, s'_2)\)、したがって、\(s \in (s_1, s_2) \cap [s'_1, s'_2)\)。
\(s_1 \lt s\)および\(s'_1 \le s\)、もしも、\((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\)および\(s \lt s'_2\)、もしも、\(s \lt Min (s_2, s'_2)\)である場合、そしてその場合に限って。
したがって、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \lt s'_2\)、もしも、\((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\)および\(s \lt Min (s_2, s'_2)\)である場合、そしてその場合に限って、もしも、\(s_1 \lt s'_1 \land s'_1 \le s \land s \lt Min (s_2, s'_2)\)または\(s'_1 \le s_1 \land s_1 \lt s \land s \lt Min (s_2, s'_2)\)である場合、そしてその場合に限って。
\(s_1 \lt s'_1\)または\(s'_1 \le s_1\)、そして、\(s_1 \lt s'_1\)である時は、\(s \in (s_1, s_2) \cap [s'_1, s'_2)\)、もしも、\(s'_1 \le s \land s \lt Min (s_2, s'_2)\)である場合、そしてその場合に限って; \(s'_1 \le s_1\)である時は、\(s \in (s_1, s_2) \cap [s'_1, s'_2)\)、もしも、\(s_1 \lt s \land s \lt Min (s_2, s'_2)\)である場合、そしてその場合に限って。
\(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)\}\)。
その上\(s'_1 \lt Min (s_2, s'_2)\)である時は、\(= [s'_1, Min (s_2, s'_2))\)。
その上\(Min (s_2, s'_2) \le s'_1\)である時は、\(= \emptyset\)。
\(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)\}\)。
その上\(s_1 \lt Min (s_2, s'_2)\)である時は、\(= (s_1, Min (s_2, s'_2))\)。
その上\(Min (s_2, s'_2) \le s_1\)である時は、\(= \emptyset\)。
ステップ4:
各\(s \in S\)に対して、\(s \in (s_1, s_2) \cap [s'_1, s'_2]\)、もしも、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \le s'_2\)である場合、そしてその場合に限って、なぜなら、もしも、\(s \in (s_1, s_2) \cap [s'_1, s'_2]\)である場合、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \le s'_2\); もしも、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \le s'_2\)である場合、\(s \in (s_1, s_2)\)および\(s \in [s'_1, s'_2]\)、したがって、\(s \in (s_1, s_2) \cap [s'_1, s'_2]\)。
\(s_1 \lt s\)および\(s'_1 \le s\)、もしも、\((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\)および\(s \le s'_2\)、もしも、\((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\)である場合、そしてその場合に限って。
したがって、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \le s'_2\)、もしも、\((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\)および\((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\)である場合、そしてその場合に限って、もしも、\(s_1 \lt s'_1 \land s'_1 \le s \land s_2 \le s'_2 \land s \lt s_2\)または\(s_1 \lt s'_1 \land s'_1 \le s \land s'_2 \lt s_2 \land s \le s'_2\)または\(s'_1 \le s_1 \land s_1 \lt s \land s_2 \le s'_2 \land s \lt s_2\)または\(s'_1 \le s_1 \land s_1 \lt s \land s'_2 \lt s_2 \land s \le s'_2\)である場合、そしてその場合に限って、もしも、\(s_1 \lt s'_1 \land s_2 \le s'_2 \land s'_1 \le s \land s \lt s_2\)または\(s_1 \lt s'_1 \land s'_2 \lt s_2 \land s'_1 \le s \land s \le s'_2\)または\(s'_1 \le s_1 \land s_2 \le s'_2 \land s_1 \lt s \land s \lt s_2\)または\(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\)または\(s_1 \lt s'_1 \land s'_2 \lt s_2\)または\(s'_1 \le s_1 \land s_2 \le s'_2\)または\(s'_1 \le s_1 \land s'_2 \lt s_2\)、そして、\(s_1 \lt s'_1 \land s_2 \le s'_2\)である時は、\(s \in (s_1, s_2) \cap [s'_1, s'_2]\)、もしも、\(s'_1 \le s \land s \lt s_2\)である場合、そしてその場合に限って; \(s_1 \lt s'_1 \land s'_2 \lt s_2\)である時は、\(s \in (s_1, s_2) \cap [s'_1, s'_2]\)、もしも、\(s'_1 \le s \land s \le s'_2\)である場合、そしてその場合に限って; \(s'_1 \le s_1 \land s_2 \le s'_2\)である時は、\(s \in (s_1, s_2) \cap [s'_1, s'_2]\)、もしも、\(s_1 \lt s \land s \lt s_2\)である場合、そしてその場合に限って; \(s'_1 \le s_1 \land s'_2 \lt s_2\)である時は、\(s \in (s_1, s_2) \cap [s'_1, s'_2]\)、もしも、\(s_1 \lt s \land s \le s'_2\)である場合、そしてその場合に限って。
\(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\}\)。
その上\(s'_1 \lt s_2\)である時は、\(= [s'_1, s_2)\)。
その上\(s_2 \le s'_1\)である時は、\(= \emptyset\)。
\(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\}\)。
その上\(s'_1 \le s'_2\)である時は、\(= [s'_1, s'_2]\)。
その上\(s'_2 \lt s'_1\)である時は、\(= \emptyset\)。
\(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\}\)。
その上\(s_1 \lt s_2\)である時は、\(= (s_1, s_2)\)。
その上\(s_2 \le s_1\)である時は、\(= \emptyset\)。
\(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\}\)。
その上\(s_1 \lt s'_2\)である時は、\(= (s_1, s'_2]\)。
その上\(s'_2 \le s_1\)である時は、\(= \emptyset\)。
ステップ5:
各\(s \in S\)に対して、\(s \in (s_1, s_2] \cap (s'_1, s'_2]\)、もしも、\(s_1 \lt s\)および\(s'_1 \lt s\)および\(s \le s_2\)および\(s \le s'_2\)である場合、そしてその場合に限って、なぜなら、もしも、\(s \in (s_1, s_2] \cap (s'_1, s'_2]\)である場合、\(s_1 \lt s\)および\(s'_1 \lt s\)および\(s \le s_2\)および\(s \le s'_2\); もしも、\(s_1 \lt s\)および\(s'_1 \lt s\)および\(s \le s_2\)および\(s \le s'_2\)である場合、\(s \in (s_1, s_2]\)および\(s \in (s'_1, s'_2]\)、したがって、\(s \in (s_1, s_2] \cap (s'_1, s'_2]\)。
\(s_1 \lt s\)および\(s'_1 \lt s\)、もしも、\(Max (s_1, s'_1) \lt s\)である場合、そしてその場合に限って。
\(s \le s_2\)および\(s \le s'_2\)、もしも、\(s \le Min (s_2, s'_2)\)である場合、そしてその場合に限って。
したがって、\(s_1 \lt s\)および\(s'_1 \lt s\)および\(s \le s_2\)および\(s \le s'_2\)、もしも、\(Max (s_1, s'_1) \lt s\)および\(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)\}\)。
\(Max (s_1, s'_1) \lt Min (s_2, s'_2)\)である時は、\(= (Max (s_1, s'_1), Min (s_2, s'_2)]\)。
\(Min (s_2, s'_2) \le Max (s_1, s'_1)\)である時は、\(= \emptyset\)。
ステップ6:
各\(s \in S\)に対して、\(s \in (s_1, s_2] \cap [s'_1, s'_2)\)、もしも、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \le s_2\)および\(s \lt s'_2\)である場合、そしてその場合に限って、なぜなら、もしも、\(s \in (s_1, s_2] \cap [s'_1, s'_2)\)である場合、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \le s_2\)および\(s \lt s'_2\); もしも、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \le s_2\)および\(s \lt s'_2\)である場合、\(s \in (s_1, s_2]\)および\(s \in [s'_1, s'_2)\)、したがって、\(s \in (s_1, s_2] \cap [s'_1, s'_2)\)。
\(s_1 \lt s\)および\(s'_1 \le s\)、もしも、\((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\)および\(s \lt s'_2\)、もしも、\((s'_2 \le s_2 \land s \lt s'_2) \lor (s_2 \lt s'_2 \land s \le s_2)\)である場合、そしてその場合に限って。
したがって、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \le s_2\)および\(s \lt s'_2\)、もしも、\((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\)および\((s'_2 \le s_2 \land s \lt s'_2) \lor (s_2 \lt s'_2 \land s \le s_2)\)である場合、そしてその場合に限って、もしも、\(s_1 \lt s'_1 \land s'_1 \le s \land s'_2 \le s_2 \land s \lt s'_2\)または\(s_1 \lt s'_1 \land s'_1 \le s \land s_2 \lt s'_2 \land s \le s_2\)または\(s'_1 \le s_1 \land s_1 \lt s \land s'_2 \le s_2 \land s \lt s'_2\)または\(s'_1 \le s_1 \land s_1 \lt s \land s_2 \lt s'_2 \land s \le s_2\)である場合、そしてその場合に限って、もしも、\(s_1 \lt s'_1 \land s'_2 \le s_2 \land s'_1 \le s \land s \lt s'_2\)または\(s_1 \lt s'_1 \land s_2 \lt s'_2 \land s'_1 \le s \land s \le s_2\)または\(s'_1 \le s_1 \land s'_2 \le s_2 \land s_1 \lt s \land s \lt s'_2\)または\(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\)または\(s_1 \lt s'_1 \land s_2 \lt s'_2\)または\(s'_1 \le s_1 \land s'_2 \le s_2\)または\(s'_1 \le s_1 \land s_2 \lt s'_2\)、そして、\(s_1 \lt s'_1 \land s'_2 \le s_2\)である時は、\(s \in (s_1, s_2] \cap [s'_1, s'_2)\)、もしも、\(s'_1 \le s \land s \lt s'_2\)である場合、そしてその場合に限って; \(s_1 \lt s'_1 \land s_2 \lt s'_2\)である時は、\(s \in (s_1, s_2] \cap [s'_1, s'_2)\)、もしも、\(s'_1 \le s \land s \le s_2\)である場合、そしてその場合に限って; \(s'_1 \le s_1 \land s'_2 \le s_2\)である時は、\(s \in (s_1, s_2] \cap [s'_1, s'_2)\)、もしも、\(s_1 \lt s \land s \lt s'_2\)である場合、そしてその場合に限って; \(s'_1 \le s_1 \land s_2 \lt s'_2\)である時は、\(s \in (s_1, s_2] \cap [s'_1, s'_2)\)、もしも、\(s_1 \lt s \land s \le s_2\)である場合、そしてその場合に限って。
\(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\}\)。
その上\(s'_1 \lt s'_2\)である時は、\(= [s'_1, s'_2)\)。
その上\(s'_2 \le s'_1\)である時は、\(= \emptyset\)。
\(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\}\)。
その上\(s'_1 \le s_2\)である時は、\(= [s'_1, s_2]\)。
その上\(s_2 \lt s'_1\)である時は、\(= \emptyset\)。
\(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\}\)。
その上\(s_1 \lt s'_2\)である時は、\(= (s_1, s'_2)\)。
その上\(s'_2 \le s_1\)である時は、\(= \emptyset\)。
\(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\}\)。
その上\(s_1 \lt s_2\)である時は、\(= (s_1 \lt s_2]\)。
その上\(s_2 \le s_1\)である時は、\(= \emptyset\)。
ステップ7:
各\(s \in S\)に対して、\(s \in (s_1, s_2] \cap [s'_1, s'_2]\)、もしも、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \le s_2\)および\(s \le s'_2\)である場合、そしてその場合に限って、なぜなら、もしも、\(s \in (s_1, s_2] \cap [s'_1, s'_2]\)である場合、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \le s_2\)および\(s \le s'_2\); もしも、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \le s_2\)および\(s \le s'_2\)である場合、\(s \in (s_1, s_2]\)および\(s \in [s'_1, s'_2]\)、したがって、\(s \in (s_1, s_2] \cap [s'_1, s'_2]\)。
\(s_1 \lt s\)および\(s'_1 \le s\)、もしも、\((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\)および\(s \le s'_2\)、もしも、\(s \le Min (s_2, s'_2)\)である場合、そしてその場合に限って。
したがって、\(s_1 \lt s\)および\(s'_1 \le s\)および\(s \le s_2\)および\(s \le s'_2\)、もしも、\((s_1 \lt s'_1 \land s'_1 \le s) \lor (s'_1 \le s_1 \land s_1 \lt s)\)および\(s \le Min (s_2, s'_2)\)である場合、そしてその場合に限って、もしも、\(s_1 \lt s'_1 \land s'_1 \le s \land s \le Min (s_2, s'_2)\)または\(s'_1 \le s_1 \land s_1 \lt s \land s \le Min (s_2, s'_2)\)である場合、そしてその場合に限って。
\(s_1 \lt s'_1\)または\(s'_1 \le s_1\)、そして、\(s_1 \lt s'_1\)である時は、\(s \in (s_1, s_2] \cap [s'_1, s'_2]\)、もしも、\(s'_1 \le s \land s \le Min (s_2, s'_2)\)である場合、そしてその場合に限って; \(s'_1 \le s_1\)である時は、\(s \in (s_1, s_2] \cap [s'_1, s'_2]\)、もしも、\(s_1 \lt s \land s \le Min (s_2, s'_2)\)である場合、そしてその場合に限って。
\(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)\}\)。
その上\(s'_1 \le Min (s_2, s'_2)\)である時は、\(= [s'_1, Min (s_2, s'_2)]\)。
その上\(Min (s_2, s'_2) \lt s'_1\)である時は、\(= \emptyset\)。
\(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)\}\)。
その上\(s_1 \lt Min (s_2, s'_2)\)である時は、\(= (s_1, Min (s_2, s'_2)]\)。
その上\(Min (s_2, s'_2) \le s_1\)である時は、\(= \emptyset\)。
ステップ8:
各\(s \in S\)に対して、\(s \in [s_1, s_2) \cap [s'_1, s'_2)\)、もしも、\(s_1 \le s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \lt s'_2\)である場合、そしてその場合に限って、なぜなら、もしも、\(s \in [s_1, s_2) \cap [s'_1, s'_2)\)である場合、\(s_1 \le s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \lt s'_2\); もしも、\(s_1 \le s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \lt s'_2\)である場合、\(s \in [s_1, s_2)\)および\(s \in [s'_1, s'_2)\)、したがって、\(s \in [s_1, s_2) \cap [s'_1, s'_2)\)。
\(s_1 \le s\)および\(s'_1 \le s\)、もしも、\(Max (s_1, s'_1) \le s\)である場合、そしてその場合に限って。
\(s \lt s_2\)および\(s \lt s'_2\)、もしも、\(s \lt Min (s_2, s'_2)\)である場合、そしてその場合に限って。
したがって、\(s_1 \le s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \lt s'_2\)、もしも、\(Max (s_1, s'_1) \lt s\)および\(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)\}\)。
\(Max (s_1, s'_1) \lt Min (s_2, s'_2)\)である時は、\(= [Max (s_1, s'_1), Min (s_2, s'_2))\)。
\(Min (s_2, s'_2) \le Max (s_1, s'_1)\)である時は、\(= \emptyset\)。
ステップ9:
各\(s \in S\)に対して、\(s \in [s_1, s_2) \cap [s'_1, s'_2]\)、もしも、\(s_1 \le s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \le s'_2\)である場合、そしてその場合に限って、なぜなら、もしも、\(s \in [s_1, s_2) \cap [s'_1, s'_2]\)である場合、\(s_1 \le s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \le s'_2\); もしも、\(s_1 \le s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \le s'_2\)である場合、\(s \in [s_1, s_2)\)および\(s \in [s'_1, s'_2]\)、したがって、\(s \in [s_1, s_2) \cap [s'_1, s'_2]\)。
\(s_1 \le s\)および\(s'_1 \le s\)、もしも、\(Max (s_1, s'_1) \le s\)である場合、そしてその場合に限って。
\(s \lt s_2\)および\(s \le s'_2\)、もしも、\((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\)である場合、そしてその場合に限って。
したがって、\(s_1 \le s\)および\(s'_1 \le s\)および\(s \lt s_2\)および\(s \le s'_2\)、もしも、\(Max (s_1, s'_1) \le s\)および\((s_2 \le s'_2 \land s \lt s_2) \lor (s'_2 \lt s_2 \land s \le s'_2)\)である場合、そしてその場合に限って、もしも、\(Max (s_1, s'_1) \le s \land s_2 \le s'_2 \land s \lt s_2\)または\(Max (s_1, s'_1) \le s \land s'_2 \lt s_2 \land s \le s'_2\)である場合、そしてその場合に限って、もしも、\(s_2 \le s'_2 \land Max (s_1, s'_1) \le s \land s \lt s_2\)または\(s'_2 \lt s_2 \land Max (s_1, s'_1) \le s \land s \le s'_2\)である場合、そしてその場合に限って。
\(s_2 \le s'_2\)または\(s'_2 \lt s_2\)、そして、\(s_2 \le s'_2\)である時は、\(s \in [s_1, s_2) \cap [s'_1, s'_2]\)、もしも、\(Max (s_1, s'_1) \le s \land s \lt s_2\)である場合、そしてその場合に限って; \(s'_2 \lt s_2\)である時は、\(s \in [s_1, s_2) \cap [s'_1, s'_2]\)、もしも、\(Max (s_1, s'_1) \le s \land s \le s'_2\)である場合、そしてその場合に限って。
\(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\}\)。
その上\(Max (s_1, s'_1) \lt s_2\)である時は、\(= [Max (s_1, s'_1), s_2)\)。
その上\(s_2 \le Max (s_1, s'_1)\)である時は、\(= \emptyset\)。
\(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\}\)。
その上\(Max (s_1, s'_1) \le s'_2\)である時は、\(= [Max (s_1, s'_1) \le s'_2]\)。
その上\(s'_2 \lt Max (s_1, s'_1)\)である時は、\(= \emptyset\)。
ステップ10:
各\(s \in S\)に対して、\(s \in [s_1, s_2] \cap [s'_1, s'_2]\)、もしも、\(s_1 \le s\)および\(s'_1 \le s\)および\(s \le s_2\)および\(s \le s'_2\)である場合、そしてその場合に限って、なぜなら、もしも、\(s \in [s_1, s_2] \cap [s'_1, s'_2]\)である場合、\(s_1 \le s\)および\(s'_1 \le s\)および\(s \le s_2\)および\(s \le s'_2\); もしも、\(s_1 \le s\)および\(s'_1 \le s\)および\(s \le s_2\)および\(s \le s'_2\)である場合、\(s \in [s_1, s_2]\)および\(s \in [s'_1, s'_2]\)、したがって、\(s \in [s_1, s_2] \cap [s'_1, s'_2]\)。
\(s_1 \le s\)および\(s'_1 \le s\)、もしも、\(Max (s_1, s'_1) \le s\)である場合、そしてその場合に限って。
\(s \le s_2\)および\(s \le s'_2\)、もしも、\(s \le Min (s_2, s'_2)\)である場合、そしてその場合に限って。
したがって、\(s_1 \le s\)および\(s'_1 \le s\)および\(s \le s_2\)および\(s \le s'_2\)、もしも、\(Max (s_1, s'_1) \le s\)および\(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)\}\)。
\(Max (s_1, s'_1) \le Min (s_2, s'_2)\)である時は、\(= [Max (s_1, s'_1), Min (s_2, s'_2)]\)。
\(Min (s_2, s'_2) \lt Max (s_1, s'_1)\)である時は、\(= \emptyset\)。
