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.