6.7　Cluster の定義

　ある mode に属性 (attribute) をいくつか附与して，新しい mode のようなもの (タイプ) を作り出すことができます．例えば，Real という mode があるとします．この mode に対して positive という属性が定義されたとしましょう．このとき，positive Real という mode (これを cluster という) も作ることができます．
　それなら positive_Real という新しい mode を作ればよさそうですが，cluster が便利なのは，

　　　x is positive_Real; then
　　　x is positive;

はいえませんが，

　　　x is positive Real; then
　　　x is positive;

は理由付けなしにいえることです．即ち，"positive Real"という cluster は positive な Real であることを，Mizar チェッカーがしっかりと覚えていてくれるのです．一度新しい cluster が定義されれば，他の articles で，environ 部の clusters のというように最初のファイル名を記入しておけば，そこで，その cluster を自由に使うことができます．
　clusters を定義する例を下に掲げます．その定義には existence だけを証明する必要があることに注意しましょう．
　なお，VOC ファイルには，あらかじめ

　　Vpositive

と書かれているものとします．

　　environ
　　　vocabulary TEST8;
　　　notation ARYTM,REAL_1;
　　　constructors ARYTM;
　　　theorems REAL_1,AXIOMS;
　　　requirements ARYTM;
　　begin
　　　definition let x be Real;
　　　　attr x is positive means　:A1: 0<x;
　　end;
　　definition
　　　cluster positive Real
　　　existence
　　　proof take 1; thus O<1; end;
　　end;
　　theorem for x,y begin positive Real
　　　holds x+y is positive Real
　　proof let x,y is positive Real;
　　　B1:0くx by A1; then 0くy by A1; then
　　　x<x+y by REAL_1:69; then
　　　0<x+y by B1, AXIOMS:22;
　　hence x+y is positive Real by A1;
　　end: