Mizar/演習/1

簡単な証明。以下の証明は当然エラーが出ない。なお、A1はラベルである。

environ
begin
  for x,y being set st x = y holds y = x
proof
 let x,y be set;
 assume
  A1: x = y;
 thus y = x by A1;
end;

数式記号	beginの中では	proofの中では
∀ ～∈...	for ～ being ...	let ～ be ...
～ ⇒	～ holds	assume ～
⇒ ～	holds ～	thus ～

なぜ、このように表現するかはトートロジーを学べば理解できるようになる。 即ち、∀ x,y は削除出来て、また、

A⇒B

とは

￢A ∨ B

を示す。