set E = TheEqSymbOf S;
A1: abs (- 2) = - (- 2) by ABSVALUE:def 1
.= 2 ;
abs (ar (TheEqSymbOf S)) = 2 by A1, FOMODEL1:def 23;
hence for b₁ being number st b₁ = (abs (ar (TheEqSymbOf S))) - 2 holds
b₁ is empty ; :: thesis: verum