set E = TheEqSymbOf S;
set N = TheNorSymbOf S;
set f = the adicity of S;
( the adicity of S c= the adicity of S & TheEqSymbOf S = TheEqSymbOf S & TheNorSymbOf S = TheNorSymbOf S ) ;
hence for b₁ being Language-like st b₁ = S null holds
b₁ is S -extending by DefExt0; :: thesis: verum