5.4　証明中の mode の宣言

　証明中に変数の mode を宣言することがよくあります．また証明のスケルトンに入りますけれども，例えば p⊆q の証明で，

　　　　P c=　Q
　　　　 proof
　　　　　let x be set;
　　　　　assume x in P;
　　　　　......
　　　　　thus x in Q;
　　　　end;


　のとき, 3行目で let x be set; としています．

　　be mode 名

　で証明中に mode を宣言することもできます．もちろん，前もって reserve x for set とすることも出来ます．