4.11 About Take

Although it becomes the repeat of Section 4.7, we explain in more detail about take.

ex r bring Real st 1<r-1
-------(1)

When proving a formula (1), we write it as follows.

theorem ex r being Real 1<r-1
proof 1+1<3;then A1:1+1-1<3-1 by REAL_1:59;
take　3;
thus 1く3-1 by REAL_2:17,A1;
end:

We have to keep in mind that the last formula is as follows instead of the form of (1).

thus 1<3-1

It is because there is "take 3" in the middle of proof, therefore the part of existing symboles are removed, we should prove only a naked part.

If we explain it in a little more detail, it is as below.

To prove (∃x)(∃y)(f(x,y)),

proof	------ ------	a formula which should be proved in this stage is
		(∃x)(∃y)(f(x,y))
	take a ------	a formula which should be proved in this stage is
		(∃y)(f(a,y))
	------ ------
	take b ------	a formula which should be proved in this stage is
		(f(a,b))
	------ ------
	hence f(a,b);
end;

Therefore, we can do the following proof.

theorem ex r,s being Real st 1<r-1
proof take 3;
take 1;1<3;
hence thesis by REAL_2:17;
end;

Further, if we prove the part about the above-mentioned f(a,b) even if we don't use take in many cases, finally the checker will look for a and b. For example, we can also do it as follows.

theorem ex r being Real st 1<r-1
proof 1+1<3;then 1+1-1<3-1 by REAL_1:59; then
1<3-1 by REAL_2:17;
hence thesis;
end;