7.4.3 When There Is An Error
When there is an error, the error number is entered to an article in the
form of comment by using a command called ERRFLAG. We use this command
Every command can omit an extension .MIZ.
To read an error message, another file (MIZAR.MSG) needs to be viewed with an editor.