Is an article allowed to call the axiom command on a theorem the article itself has already proved? Presumably any articles in gilith won't do that though...?