for S being Language holds S -formulasOfMaxDepth 0 = AtomicFormulasOf S by Lm16;