set Q = S -sequents ;
reconsider X = SQ1, Y = SQ2 as Subset of (S -sequents) by DefSeqtLike2;
X \/ Y c= S -sequents ;
hence for b₁ being set st b₁ = SQ1 \/ SQ2 holds
b₁ is S -sequents-like ; :: thesis: verum