theorem :: FOMODEL1:14

for S being Language holds S -termsOfMaxDepth is sequence of (bool ((AllSymbolsOf S) *)) ;