6.8　structure の導入

(X,a) を二項代数とする，というような場合(X は集合,a は関数)，

　　struct Binalg(# base->set,op2->Function #);

とだけ書きます( definition　など，つけないで)．新しい用語 Binalg, base, op2 のためには VOC ファイルの中に，

　　　　GBinalg
　　　　Ubase
　　　　Uop2

と書いておきます(G,Uの種別コードをつけることに注意)．
　すると次のような定理は理由付けなしに成立します．

　　theorem for X being set, a being Function
　　holds (the base of Binalg(# X,a #))=X;

これは, 「二項代数 (X,a) のベースは X である」という命題に対応します．base に the をつけることに注意して下さい．