:: deftheorem Def4 defines -premises-like FOMODEL4:def 4 :
for S being Language
for x being set holds
( x is S -premises-like iff ( x c= AllFormulasOf S & x is finite ) );