4.12　hereby

　証明中で使われる hereby は thus + now と同じです．
　例えば，

　　theorem TT1: (for x st x in A holds x in B) & A=A \/ A
　　proof
　　　　hereby let x; assume X in A;
　　　　　hence x in B;
　　　　end;
　　　　thus A=A \/ A by BOOLE:35;
　　　end;

　では，(for x st　x in A holds x in B) の命題がまず証明されて，証明すべき命題群から除かれます．即ち，

　　　now let x;
　　　　　assume X in A;
　　　　　------
　　　　　hence x in B;
　　　end;

　の部分が，上の (for----) と同じです．これがまず証明される．ということは，

　　　thus now　---
　　　----
　　　----
　　　　　　end;

　というように thus が now の前につけられます．これは，

　　　hereby ----
　　　-----
　　　-----
　　　end;

　となるのです．
　この応用編として,次のような hereby の使い方があります(これは証明をつけるまでもなく自明な定理ですが)．


　　　theorem AA2: x=y iff not y<>x
　　　proof
　　　　hereby assume x=y;
　　　　　hence not y<>x;
　　　　end:
　　　　assume not y<>x;
　　　　hence x=y;
　　　end:

(x=y iff not y<>x) という命題は，(x=y implies not y<>x) & (not y<>x implies x=y) という命題と同じです．hereby で前の (-----) の部分が証明されて取り除かれ，後半では，後の (-----)の部分を証明するのみ，となります．
　更なる応用編として，

　　　theorem BB2: A=B
　　　proof hereby let x be Any; assume A1: x in A;
　　　　 thus x in B by TT1.A1;
　　　　end:
　　　　let x;
　　　　assume X in B;
　　　　hence x in in A by TT1;
　　　end;

があります．これは，環境部の definition 部に BOOLE があることによって，(A=B) は，(A c=B)&(B c=A) と同じとみなされます．更に definintion 部に TARSKI があることによって，これは，

　　　(for x st x in A holds x in B) &
　　　(for x st x in B holds x in A)

と同じとみなされます．この形になれば，上の例が hereby で記述できることが分かるでしょう．実際には，この最後の例のように，2つの集合が等しいことを言うときに，よく hereby が使われます．