theorem :: FOMODEL2:7

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