:: deftheorem Def3 defines -sequents-like FOMODEL4:def 3 :
for S being Language
for X being set holds
( X is S -sequents-like iff X c= S -sequents );