set Q = S -sequents ;
Sq in S -sequents by DefSeqtLike;
then {Sq} c= S -sequents by ZFMISC_1:31;
hence {Sq} is S -sequents-like ; :: thesis: verum