set Q = S -sequents ;
reconsider f = (m,D) -derivables as Function of (bool (S -sequents)),(bool (S -sequents)) ;

per cases ( not X in bool (S -sequents) or X in bool (S -sequents) ) ;

suppose not X in bool (S -sequents) ; :: thesis: ((m,D) -derivables) . X is S -sequents-like

then not X in dom f ;
then f . X = {} by FUNCT_1:def 2;
then f . X c= S -sequents by XBOOLE_1:2;
hence ((m,D) -derivables) . X is S -sequents-like ; :: thesis: verum

end;

suppose X in bool (S -sequents) ; :: thesis: ((m,D) -derivables) . X is S -sequents-like

then reconsider XX = X as Element of bool (S -sequents) ;
f . XX is Element of bool (S -sequents) ;
hence ((m,D) -derivables) . X is S -sequents-like ; :: thesis: verum

end;

end;