S -formulasOfMaxDepth 0 = AtomicFormulasOf S by Lm16;
hence for b₁ being set st b₁ = S -formulasOfMaxDepth 0 holds
b₁ is S -prefix ; :: thesis: verum