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