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