the wff exal string of S in ExFormulasOf S ;
hence for b₁ being set st b₁ = ExFormulasOf S holds
not b₁ is empty ; :: thesis: verum