:: deftheorem defines LowerCompoundersOf FOMODEL1:def 6 :
for S being Language-like holds LowerCompoundersOf S = the adicity of S " (INT \ {0});