5.4 証明中の mode の宣言
証明中に変数の mode を宣言することがよくあります．また証明のスケルトンに入りますけれども，例えば P ⊆ Q の証明で，
P c= Q
proof
let x be Any;
assume x ∈ P ;
......
thus x ∈ Q;
end;
のとき，3行目で let x be Any; としています．
be mode名
で証明中に mode を宣言することもできます．もちろん,前もって reserve x for Any とすることも出来ます．
5.4.1 c= についての注意
また注意ですが，Mizar では ⊆ の代わりに c= を使いますが，c= を使う場合は c= の前後に１つづつスペースをあける必要があります．
5.4.2 実際に definition を使っている例
それから，ここでは，(∀ x)(x ∈ P ⇒ x ∈ Q) を証明していて，P ⊆ Q を証明したわけではありません．両者のあいだには数学的距離があります．しかしこれは3章で説明したように環境部の definitions の中に TARSKI を書いておくことにより，システムが自動的に両者が同値であることを理解します．これは，TARSKI の abstract ファイル中に predicate（述語命題）としてこのことが定義されていることによります.
TARSKIには，Mizar ライブラリの基本となる定理から構成されているため，アーティクルを書くにあたっては環境部の definitions のところに TARSKI を書いておきます．