次を仮定する。$`\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\Imp}{ \Rightarrow }
`$
- $`M \subseteq \mbf{R}`$
- $`M\ne \emptyset`$
- $`M`$ は有界
- $`\alpha\in \mbf{R}`$ は $`M`$ の上界
以上すべての仮定のもとで（使わない仮定もあるが）、以下の2つの命題が同値であることを示す。混乱を避けるために、異なるスコープにある束縛変数は別な名前にしておく。共通する自由変数は $`M, \alpha`$
- [A] $`\forall \beta\in \mbf{R}.\, \beta \lt \alpha \Imp M\cap (\beta, \alpha] \ne \emptyset`$
- [B] $`\forall \gamma\in \mbf{R}.\, \gamma \lt \alpha \Imp M\cap [\gamma, \alpha] \ne \emptyset`$
命題に参照用ラベルを貼りたい場合／参照したい場合は、上記のようにブラケット内にラベルを入れる。
[A] から [B] は容易に示せるから割愛する。[B] から [A] を示す。[B] を前提する。
[A] を示すには、[1] $`\beta \lt \alpha`$ を仮定して、[2] $`M\cap (\beta, \alpha]\ne \emptyset`$ を導けばよい。
仮定 [1] と前提している（暫定的に公理扱いの）命題 [B] から次が言える。
- [3] $`M\cap [\beta, \alpha] \ne \emptyset`$
[3] は、[4] $`\beta \le x \le \alpha`$ である $`x\in M`$ の存在を主張している。$`x`$ は次の2つの場合がありえる。
- [5] $`\beta \lt x \le \alpha`$
- [6] $`\beta = x`$
[5] であれば、そこから結論 [2] が言えるので、オシマイ。[6] $`\beta = x`$ の場合を考える。
もし、[7] $`x \lt x'`$ となる $`x'\in M`$ が取れる（存在する）なら、$`x`$ を $`x'`$ に取り直して [5'] $`\beta \lt x' \le \alpha`$ が言える。その場合は [5'] から結論 [2] が言えるので、オシマイ。
残る場合は、[7] $`x \lt x'`$ となる $`x'\in M`$ が取れない（存在しない）場合。この場合は結論 [2] は言えない。しかし、そんな場合が起こるのか？
今 $`\beta' := (\beta + \alpha)/2 = (x + \alpha)/2`$ と取ると、$`x \lt \beta' \lt \alpha`$ となる。前提して（暫定的に公理扱いして）いる [B] から、[8] $`M\cap [\beta', \alpha] \ne \emptyset`$ となる。これは、[7] $`\beta = x \lt x' \le \alpha`$ となる $`x'\in M`$ が取れる（存在している）ことを意味する。
つまり、$`\beta = x`$ である場合でも、$`x \lt x' \le \alpha`$ となる $`x'\in M`$ を取リ直して、その $`x'`$ に関して $`\beta \lt x' \le \alpha`$ が言える。これで結論 [2] が導けたので [A] が示せた。
結局、上限の定義に閉区間を使うか半開区間を使うかは、定義の論理的内容には影響しない。どちらを使うかは恣意的な選択となる。
