set Q = S -sequents ;
reconsider X = SQ1, Y = SQ2 as Subset of (S -sequents) by Def3;
X \/ Y c= S -sequents ;
hence SQ1 \/ SQ2 is S -sequents-like ; :: thesis: verum