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;