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.