In order to be more 'user-friendly', MATHsAiD provides two displays for each axiom/theorem/fact/etc., primarily in recognition of the fact that information readable by a computer system is not necessarily so easily readable by humans. The lower display shows all the (ASCII) information needed by the system in order to function properly, whereas the upper display shows a 'latex-like' version of this information, typically in somewhat less detail. The latter more or less corresponds to the abbreviations/simplified notation which mathematicians prefer to write/look at, whereas in their minds, they realise the 'full/precise' notation (something like the lower display). Note that the 'latex-like' version is produced by the system itself, according to instructions provided by the user.
We draw attention to Theorem 15 above; this is the 'Zariski space result' mentioned before, which first appeared in a refereed mathematics journal several years ago, following its discovery by two of the MATHsAiD project members, together with a fellow colleague (who is now, sadly, no longer with us).