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
hereby let x; assume X in A;
hence x in B;
thus A=A \/ A by BOOLE:35;
Thus, the following part is the same as (for -----) above.
now let x;
assume X in A;
hence x in B;
"This is proved first" means that we can attach thus before now as follows.
thus now ---
This become as follows.
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
hereby assume x=y;
hence not y<>x;
assume not y<>x;
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;
assume X in B;
hence x in in A by TT1;
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.