There is a multitude of kinds of facts in the reality of mankind. We do not suppose that each kind is expressible in the Lingua Cosmica discussed in the present treatise. This is because we are concerned with facts in a logical sense. Facts expressible in LINCOS consist as we have seen in examples in PART I nearly always of an implication or a sequence of implications leading from premises to a conclusion, written to the right of the rightmost implication token. The premises, i.e. one or more terms to the left of the token, contain necessary (not necessarily sufficient) information by which the conclusion can be verified. Other information may be needed; it should be available in and extractible from the environment (a logical database), sometimes in this treatise called the stage, see Chap. 7 and especially Chap. 8. The present chapter provides information on the way facts of a simple kind are introduced, verified and applied. We have already briefly mentioned and described some conventions around the concept of facts. Now we introduce in more detail and more systematically the topics of facts, lemma’s or theorems and their verifications.