set E = TheEqSymbOf S;
ar (TheEqSymbOf S) = - 2 by FOMODEL1:def 23;
hence for b₁ being number st b₁ = (ar (TheEqSymbOf S)) + 2 holds
b₁ is zero ; :: thesis: verum