set O = OneStep D;
set All = union (((OneStep D) [*]) .: {X});
set Q = S -sequents ;
B0: ((m,D) -derivables) . X c= S -sequents by DefSeqtLike2;
let x be set ; :: thesis: ( x is m,X,D -derivable implies x is S -sequent-like )
assume x is m,X,D -derivable ; :: thesis: x is S -sequent-like
then x in ((m,D) -derivables) . X by DefDerivable3;
hence x is S -sequent-like by B0; :: thesis: verum