:: deftheorem Def2 defines -sequent-like FOMODEL4:def 2 :
for S being Language
for x being object holds
( x is S -sequent-like iff x in S -sequents );