theorem :: FOMODEL1:7

for S being Language holds AllTermsOf S is S -prefix ;