Lemma fileDescription1InvariantsEndNotSection : endSectionFileNotSection fileDescription1.
