一階論理から始め、集合・クラスの基本的な扱いまでを整備します。(dagger)
集合・クラスについては「ZFとそのメタ」（あるいはNGB）に準拠します。
当システムは、例えば空集合公理の代わりとしてというwordとその定義.を置きます。
集合をクラスとみなす仕組みも作られ、集合の関数をクラスの関数から誘導することもあります。(dagger)
\(\mathbb{W}_0\)(p,p) … \(\neg\)
\(\mathbb{W}_0\)(pp,p) … \(,\) \({\bf ,}\) \(\mathbin{\rm o\!r}\) \(\Rightarrow\) \(\Longrightarrow\) \(\Leftrightarrow\) \(\Longleftrightarrow\)
\(\mathbb{W}_0\)(ss,p) … \(=\)
\(\mathbb{W}_1\)(cc,p) … \(=\)
abbr … \(\begin{cases} P_{1} \\ \vdots \\ P_{\tt n} \end{cases}\) ≈ \(( P_{1} ) , \cdots , ( P_{\tt n} )\)
abbr … \(X_{1} , \cdots , X_{\tt n} \mathop{{\sf A}}\) ≈ \(X_{1} \mathop{{\sf A}} , \cdots , X_{\tt n} \mathop{{\sf A}}\)
abbr … \(X_{1} \mathbin{{\sf p}} X_{2} \cdots \mathbin{{\sf p}} X_{\tt n}\) ≈ \(( X_{1} \mathbin{{\sf p}} X_{2} ) , \cdots , ( X_{\tt n\,{\text -}\,1} \mathbin{{\sf p}} X_{\tt n} )\)
abbr … \(X \mathbin{{\sf p}} Y \mathbin{{\sf q}} Z\) ≈ \(( X \mathbin{{\sf p}} Y ) , ( Y \mathbin{{\sf q}} Z )\)
lower … \(A \stackrel{{\tt /}}{\mathbin{{\sf p}}} B\) ≃ \(\neg ( A \mathbin{{\sf p}} B )\)
\(\mathbb{W}_2\)(\({\tt x}\)\({\tt y}\),\({\tt z}\)→\({\tt y}\)\({\tt x}\),\({\tt z}\)) … \(\leftrightarrow\)
lower … \(A \stackrel{\leftrightarrow}{\mathbin{{\sf p}}} B\) ≃ \(B \mathbin{{\sf p}} A\)
\(\mathbb{W}_2\)(\({\tt x}\)\({\tt x}\),\({\tt y}\)→\({\tt x}\),\({\tt y}\)) … \(\prime\prime\)
lower … \(\stackrel{\prime\prime}{\mathbin{{\sf p}}} A\) ≃ \(A \mathbin{{\sf p}} A\)
1以上の自然数 \({\tt n}\) に対し
abbr … \(\forall x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( P )\)
abbr … \(\exists x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( P )\)
abbr … \(\forall x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} \mathop{{\sf A}} , \cdots , x_{\tt n} \mathop{{\sf A}} \Longrightarrow ( P ) )\)
abbr … \(\exists x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( x_{1} \mathop{{\sf A}} , \cdots , x_{\tt n} \mathop{{\sf A}} , ( P ) )\)
2以上の自然数 \({\tt n}\) に対し
abbr … \(\forall^* x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} \Longrightarrow ( P ) )\)
abbr … \(\exists^* x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} , ( P ) )\)
abbr … \(\forall^* x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\forall x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} \Longrightarrow ( P ) )\)
abbr … \(\exists^* x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\exists x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} , ( P ) )\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)
abbr … \(\{ x \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , ( P ) \}\)
以下の2つの左辺では \(\mathop{{\sf X}}\) が表記上無視されます。
abbr … \(\{ T \mid P \}\) ≈ \(\{ x \mid \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
abbr … \(\{ T \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
次のものの左辺は特殊表記されています。
abbr … \(_{ P } T\) ≈ \(\{ T \mid P \}\)
\(\mathbb{W}_0\)(ss,p) … \(\in\)
\(\mathbb{W}_1\)(sc,p) … \(\in\)
cvt … \(X \in \{ x \mid P \}\) ≃ \(P\) の \(x\) に \(X\) を代入したもの
am1. … \(! x P \Longleftrightarrow \forall y , z \in \{ x \mid P \} . y = z\)
exi!. … \(\exists! x P \Longleftrightarrow \exists x P , ! x P\)
abbr … \(! x \mathop{{\sf A}} . P\) ≈ \(! x ( x \mathop{{\sf A}} , ( P ) )\)
abbr … \(\exists! x \mathop{{\sf A}} . P\) ≈ \(\exists! x ( x \mathop{{\sf A}} , ( P ) )\)
lower … \(\stackrel{\text{^}}{\mathbin{{\sf f}}} A\) ≃ \(\{ \mathbin{{\sf f}} a \mid a \in A \}\)
\(\dot\exists \stackrel{\text{^}}{\mathop{{\sf f}}} A\) というのが置換公理です(？)
\(\mathbb{W}_2\)(ss,s→ss,c) … \(\text{^*}\) \(\text{*^}\) \(\text{^^}\)
lower … \(A \stackrel{\text{^*}}{\mathbin{{\sf f}}} b\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A \}\)
lower … \(a \stackrel{\text{*^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid b \in B \}\)
lower … \(A \stackrel{\text{^^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A , b \in B \}\)
abbr … \([ x \mapsto X ]\) ≈ \(\mathsf{fn} \, x \, ( X )\)
cvt … \([ x \mapsto X ] ( T )\) ≃ \(T\) の \(x\) に \(X\) を代入したもの
\(\mapsto\) の前のv-Formを \(\bullet\) に替えられます。その際 \(\bullet \mapsto\) は略されます。
例 \([ \bullet + a ]\) ≈ \([ x \mapsto x + a ]\)
\(\bullet\) は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例 \([ \bullet + [ \bullet + a ] ( x ) ]\) ≃ \([ \bullet + ( x + a ) ]\)
lower … \({\mathbin{{\sf f}}} \stackrel{\star}{\mathbin{{\sf a}}} {\mathbin{{\sf g}}}\) ≃ \(\forall x ( ( \mathbin{{\sf f}} x ) \mathbin{{\sf a}} ( \mathbin{{\sf g}} x ) )\)
\(\mathbb{W}_2\)(\({\tt x}\)\({\tt x}\),\({\tt y}\)→[ff,\({\tt x}\)][ff,\({\tt x}\)],\({\tt y}\)) … \(\star\!\star\)
lower … \({\mathbin{{\sf f}}} \stackrel{\star\!\star}{\mathbin{{\sf a}}} {\mathbin{{\sf g}}}\) ≃ \(\forall x , y ( ( x \mathbin{{\sf f}} y ) \mathbin{{\sf a}} ( x \mathbin{{\sf g}} y ) )\)
lower … \({\mathbin{{\sf p}}} :\mathsf{R}\) ≃ \(\forall x ( x \mathbin{{\sf p}} x )\)
lower … \({\mathbin{{\sf p}}} :\mathsf{T}\) ≃ \(\forall x , y , z ( x \mathbin{{\sf p}} y \mathbin{{\sf p}} z \Longrightarrow x \mathbin{{\sf p}} z )\)
lower … \({\mathbin{{\sf p}}} :\mathsf{X}\) ≃ \(\forall x , y ( x \mathbin{{\sf p}} y \Longrightarrow y \mathbin{{\sf p}} x )\)
\({ \mathbin{p} } :\mathsf{R} \Longleftrightarrow [ \bullet ] \stackrel{\star}{\mathbin{p}} [ \bullet ]\) \(\blacktriangleleft\) O
\({ \mathbin{p} } :\mathsf{R} \Longleftrightarrow {=} \stackrel{\star\!\star}{\Rightarrow} { \mathbin{p} }\) \(\blacktriangleleft\) O
次のようなlowerは自動で追加されます。
lower … \({\mathbin{{\sf p}}} :\mathsf{R}\&\mathsf{T}\) ≃ \({\mathbin{{\sf p}}} :\mathsf{R} , {\mathbin{{\sf p}}} :\mathsf{T}\)
\({=} :\mathsf{R}\&\mathsf{T}\&\mathsf{X}\) \(\blacktriangleleft\) O
Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます。
=. … \({=} \stackrel{\star\!\star}{\Leftrightarrow} {=}\)
sub_. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
subn_. … \(X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y\)
\(\mathbb{W}_0\)(ss,p) … \(\subset\) \(\subsetneq\)
sub. … \({\subset} \stackrel{\star\!\star}{\Leftrightarrow} {\subset}\)
subn. … \({\subsetneq} \stackrel{\star\!\star}{\Leftrightarrow} {\subsetneq}\)
subn.. … \(X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\({\subset} :\mathsf{R}\&\mathsf{T}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
=.. … \(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \subsetneq Y \subset Z \mathbin{\rm o\!r} X \subset Y \subsetneq Z \Longrightarrow X \subsetneq Z\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
Thm査読
集合・クラスについては「ZFとそのメタ」（あるいはNGB）に準拠します。
当システムは、例えば空集合公理の代わりとしてというwordとその定義.を置きます。
集合をクラスとみなす仕組みも作られ、集合の関数をクラスの関数から誘導することもあります。(dagger)
a
命題記号、等号
\(\mathbb{W}_0\)(,p) … \(\top\) \({\perp}\)\(\mathbb{W}_0\)(p,p) … \(\neg\)
\(\mathbb{W}_0\)(pp,p) … \(,\) \({\bf ,}\) \(\mathbin{\rm o\!r}\) \(\Rightarrow\) \(\Longrightarrow\) \(\Leftrightarrow\) \(\Longleftrightarrow\)
\(\mathbb{W}_0\)(ss,p) … \(=\)
\(\mathbb{W}_1\)(cc,p) … \(=\)
andを含む略記
2以上の自然数 \({\tt n}\) に対しabbr … \(\begin{cases} P_{1} \\ \vdots \\ P_{\tt n} \end{cases}\) ≈ \(( P_{1} ) , \cdots , ( P_{\tt n} )\)
abbr … \(X_{1} , \cdots , X_{\tt n} \mathop{{\sf A}}\) ≈ \(X_{1} \mathop{{\sf A}} , \cdots , X_{\tt n} \mathop{{\sf A}}\)
abbr … \(X_{1} \mathbin{{\sf p}} X_{2} \cdots \mathbin{{\sf p}} X_{\tt n}\) ≈ \(( X_{1} \mathbin{{\sf p}} X_{2} ) , \cdots , ( X_{\tt n\,{\text -}\,1} \mathbin{{\sf p}} X_{\tt n} )\)
abbr … \(X \mathbin{{\sf p}} Y \mathbin{{\sf q}} Z\) ≈ \(( X \mathbin{{\sf p}} Y ) , ( Y \mathbin{{\sf q}} Z )\)
2項記号の処理
\(\mathbb{W}_2\)(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)lower … \(A \stackrel{{\tt /}}{\mathbin{{\sf p}}} B\) ≃ \(\neg ( A \mathbin{{\sf p}} B )\)
\(\mathbb{W}_2\)(\({\tt x}\)\({\tt y}\),\({\tt z}\)→\({\tt y}\)\({\tt x}\),\({\tt z}\)) … \(\leftrightarrow\)
lower … \(A \stackrel{\leftrightarrow}{\mathbin{{\sf p}}} B\) ≃ \(B \mathbin{{\sf p}} A\)
\(\mathbb{W}_2\)(\({\tt x}\)\({\tt x}\),\({\tt y}\)→\({\tt x}\),\({\tt y}\)) … \(\prime\prime\)
lower … \(\stackrel{\prime\prime}{\mathbin{{\sf p}}} A\) ≃ \(A \mathbin{{\sf p}} A\)
全称量化子、存在量化子
\(\mathbb{W}_0\)(vp,p)R … \(\forall\) \(\exists\)1以上の自然数 \({\tt n}\) に対し
abbr … \(\forall x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( P )\)
abbr … \(\exists x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( P )\)
abbr … \(\forall x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} \mathop{{\sf A}} , \cdots , x_{\tt n} \mathop{{\sf A}} \Longrightarrow ( P ) )\)
abbr … \(\exists x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( x_{1} \mathop{{\sf A}} , \cdots , x_{\tt n} \mathop{{\sf A}} , ( P ) )\)
2以上の自然数 \({\tt n}\) に対し
abbr … \(\forall^* x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} \Longrightarrow ( P ) )\)
abbr … \(\exists^* x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} , ( P ) )\)
abbr … \(\forall^* x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\forall x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} \Longrightarrow ( P ) )\)
abbr … \(\exists^* x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\exists x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} , ( P ) )\)
b
クラス
\(\mathbb{W}_1\)(vp,c)F … \(\mathsf{cls}\)abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)
abbr … \(\{ x \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , ( P ) \}\)
以下の2つの左辺では \(\mathop{{\sf X}}\) が表記上無視されます。
abbr … \(\{ T \mid P \}\) ≈ \(\{ x \mid \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
abbr … \(\{ T \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
次のものの左辺は特殊表記されています。
abbr … \(_{ P } T\) ≈ \(\{ T \mid P \}\)
\(\mathbb{W}_0\)(ss,p) … \(\in\)
\(\mathbb{W}_1\)(sc,p) … \(\in\)
cvt … \(X \in \{ x \mid P \}\) ≃ \(P\) の \(x\) に \(X\) を代入したもの
一意量化子
\(\mathbb{W}_1\)(vp,p)R … \(!\) \(\exists!\)am1. … \(! x P \Longleftrightarrow \forall y , z \in \{ x \mid P \} . y = z\)
exi!. … \(\exists! x P \Longleftrightarrow \exists x P , ! x P\)
abbr … \(! x \mathop{{\sf A}} . P\) ≈ \(! x ( x \mathop{{\sf A}} , ( P ) )\)
abbr … \(\exists! x \mathop{{\sf A}} . P\) ≈ \(\exists! x ( x \mathop{{\sf A}} , ( P ) )\)
関数の像
\(\mathbb{W}_2\)(s,s→s,c) … \(\text{^}\)lower … \(\stackrel{\text{^}}{\mathbin{{\sf f}}} A\) ≃ \(\{ \mathbin{{\sf f}} a \mid a \in A \}\)
\(\dot\exists \stackrel{\text{^}}{\mathop{{\sf f}}} A\) というのが置換公理です(？)
\(\mathbb{W}_2\)(ss,s→ss,c) … \(\text{^*}\) \(\text{*^}\) \(\text{^^}\)
lower … \(A \stackrel{\text{^*}}{\mathbin{{\sf f}}} b\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A \}\)
lower … \(a \stackrel{\text{*^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid b \in B \}\)
lower … \(A \stackrel{\text{^^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A , b \in B \}\)
アロー関数
\(\mathbb{W}_1\)(vs,(s,s)) … \(\mathsf{fn}\)abbr … \([ x \mapsto X ]\) ≈ \(\mathsf{fn} \, x \, ( X )\)
cvt … \([ x \mapsto X ] ( T )\) ≃ \(T\) の \(x\) に \(X\) を代入したもの
\(\mapsto\) の前のv-Formを \(\bullet\) に替えられます。その際 \(\bullet \mapsto\) は略されます。
例 \([ \bullet + a ]\) ≈ \([ x \mapsto x + a ]\)
\(\bullet\) は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例 \([ \bullet + [ \bullet + a ] ( x ) ]\) ≃ \([ \bullet + ( x + a ) ]\)
c
2項記号の関数化
\(\mathbb{W}_2\)(\({\tt x}\)\({\tt x}\),\({\tt y}\)→[f,\({\tt x}\)][f,\({\tt x}\)],\({\tt y}\)) … \(\star\)lower … \({\mathbin{{\sf f}}} \stackrel{\star}{\mathbin{{\sf a}}} {\mathbin{{\sf g}}}\) ≃ \(\forall x ( ( \mathbin{{\sf f}} x ) \mathbin{{\sf a}} ( \mathbin{{\sf g}} x ) )\)
\(\mathbb{W}_2\)(\({\tt x}\)\({\tt x}\),\({\tt y}\)→[ff,\({\tt x}\)][ff,\({\tt x}\)],\({\tt y}\)) … \(\star\!\star\)
lower … \({\mathbin{{\sf f}}} \stackrel{\star\!\star}{\mathbin{{\sf a}}} {\mathbin{{\sf g}}}\) ≃ \(\forall x , y ( ( x \mathbin{{\sf f}} y ) \mathbin{{\sf a}} ( x \mathbin{{\sf g}} y ) )\)
2項述語の1項述語
\(\mathbb{W}_2\)([ss,p],p)R … \(:\mathsf{R}\) \(:\mathsf{T}\) \(:\mathsf{X}\)lower … \({\mathbin{{\sf p}}} :\mathsf{R}\) ≃ \(\forall x ( x \mathbin{{\sf p}} x )\)
lower … \({\mathbin{{\sf p}}} :\mathsf{T}\) ≃ \(\forall x , y , z ( x \mathbin{{\sf p}} y \mathbin{{\sf p}} z \Longrightarrow x \mathbin{{\sf p}} z )\)
lower … \({\mathbin{{\sf p}}} :\mathsf{X}\) ≃ \(\forall x , y ( x \mathbin{{\sf p}} y \Longrightarrow y \mathbin{{\sf p}} x )\)
\({ \mathbin{p} } :\mathsf{R} \Longleftrightarrow [ \bullet ] \stackrel{\star}{\mathbin{p}} [ \bullet ]\) \(\blacktriangleleft\) O
\({ \mathbin{p} } :\mathsf{R} \Longleftrightarrow {=} \stackrel{\star\!\star}{\Rightarrow} { \mathbin{p} }\) \(\blacktriangleleft\) O
次のようなlowerは自動で追加されます。
lower … \({\mathbin{{\sf p}}} :\mathsf{R}\&\mathsf{T}\) ≃ \({\mathbin{{\sf p}}} :\mathsf{R} , {\mathbin{{\sf p}}} :\mathsf{T}\)
\({=} :\mathsf{R}\&\mathsf{T}\&\mathsf{X}\) \(\blacktriangleleft\) O
外延性公理
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます。
=. … \({=} \stackrel{\star\!\star}{\Leftrightarrow} {=}\)
包含関係
\(\mathbb{W}_1\)(cc,p) … \(\subset\) \(\subsetneq\)sub_. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
subn_. … \(X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y\)
\(\mathbb{W}_0\)(ss,p) … \(\subset\) \(\subsetneq\)
sub. … \({\subset} \stackrel{\star\!\star}{\Leftrightarrow} {\subset}\)
subn. … \({\subsetneq} \stackrel{\star\!\star}{\Leftrightarrow} {\subsetneq}\)
subn.. … \(X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\({\subset} :\mathsf{R}\&\mathsf{T}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
=.. … \(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \subsetneq Y \subset Z \mathbin{\rm o\!r} X \subset Y \subsetneq Z \Longrightarrow X \subsetneq Z\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
Thm査読