4.9 Method for Using @proof

When we write a long article in Mizar, we end up checking constantly with a Mizar checker. It takes time to check a long article; therefore, by skipping the check of definitions that have already been demonstrated, we can save some time when checking in Mizar.
    To omit checking definitions and others, we replace proof with @proof. By doing this, the Mizar checker will not check that definition.
    Of course, when articles are completed, all the @proof need to be removed.