4.12 Hereby

Hereby used in proof is the same as thus + now.
For example, at the following the proposition of (for x st x in A holds x in B) is first proved and it will be removed from the proposition group that should be proved.

      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;

Thus, the following part is the same as (for -----) above.

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

"This is proved first" means that we can attach thus before now as follows.

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

This become as follows.

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

There are the following ways of using hereby as a application course (This does not need to prove and is an obvious theorem.).

      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:

The proposition (x=y iff not y<>x) is the same as a proposition called (x=y implies not y<>x)&(not y<>x implies x=y). The former (-----) part is proved and removed by hereby, and we are proving the latter (-----) part in the second half.
    As the further application course, there is the following.

      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;

This is regarded as (A=B) being the same as (A c=B)&(B c=A), because the definition section of an environ section has BOOLE. Furthermore, because the definintion section has TARSKI, it is considered that this is the same as the following.

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

If it becomes this form, it will turn out that the above-mentioned example can describe by hereby. Actually, When we describe that two sets are equallike this last example, hereby is often used.