set Q = S -sequents ;
X c= S -sequents by Def3;
then X /\ Y c= S -sequents by XBOOLE_1:1;
hence X /\ Y is S -sequents-like ; :: thesis: verum