:: deftheorem defines -sequents FOMODEL4:def 1 :
for S being Language holds S -sequents = { [premises,conclusion] where premises is Subset of (AllFormulasOf S), conclusion is wff string of S : premises is finite } ;