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.