set O = OneStep D;
set All = union (((OneStep D) [*]) .: {X});
set Q = S -sequents ;
A1: ((m,D) -derivables) . X c= S -sequents by Def3;
let x be object ; :: 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 ;
hence x is S -sequent-like by A1; :: thesis: verum