(S -formulasOfMaxDepth 0) \ (AllFormulasOf S) = {} ;
hence for b₁ being set st b₁ = (AtomicFormulasOf S) \ (AllFormulasOf S) holds
b₁ is empty by Lm16; :: thesis: verum