引用WIIS

定義

10反射律、11反対称律、12推移律、13完備律を備えののが大小関係。
狭義大小関係は、上に加えて同値関係が成り立たないもの。
x<y⇔x≤y∧x≠y

定理

x<y⇒¬(y<x)
の証明。

感覚的には自明なんだけど一応。
x<y⇒y<xと仮定し矛盾を導く。

x<y⇒y<x(仮定)
[x<y](仮定)
y<y(⇒除去)
(x<y)∧(y<x)(∧導入)
(x≤y)∧(y≤x)∧(x≠y∧x≠y)(<定義)
(x=y)∧(y≠x)(べき等律と反対称律)
⊥
¬(x<y)(背理法無矛盾律)①

[x<y](仮定)
[x=y](仮定)
(x≤y∧x≠y)∧(x=y)(∧導入)
⊥
¬(x<y)
x=y→¬(x<y)

x=xとした場合は①の定理から

x<x⇒¬(x<x)(仮定)
[(x<x)](仮定)
(x<x)∧¬(x<x)(∧導入)
⊥(矛盾)
¬(x<x)(背理法)

<は同じ要素の間には成り立ちません。

三分律

(x<y)∨(y<x)∨(x=y)
の証明。

x<y∧x=y(仮定)
x≤y∧∧x≠y∧x=y(<定義)
x≤y∧⊥(排中律)
⊥(べき等律)

y<y∧x=yも同様。

x<y∧y<x(仮定)
x≤y∧y≤x∧x≠y(<定義)
x=y∧x≠y(≤反対称律)
⊥(反対称律)

以上、異なる実数の狭義大小関係の性質があきらかになりました