set Q = S -sequents ;
set O = OneStep D;
set F = { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ;
let IT be set ; :: thesis: ( IT is X,D -derivable implies IT is S -sequents-like )
assume IT is X,D -derivable ; :: thesis: IT is S -sequents-like
then IT c= union (((OneStep D) [*]) .: {X}) by DefDerivable;
then B0: IT c= union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } by Lm18;

now

let x be set ; :: thesis: ( x in IT implies x in S -sequents )
assume x in IT ; :: thesis: x in S -sequents
then consider Y being set such that
C0: ( x in Y & Y in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ) by B0, TARSKI:def 4;
consider mm being Element of NAT such that
C1: Y = ((mm,D) -derivables) . X by C0;
x is mm,X,D -derivable by DefDerivable3, C0, C1;
hence x in S -sequents by DefSeqtLike; :: thesis: verum

end;

then IT c= S -sequents by TARSKI:def 3;
hence IT is S -sequents-like ; :: thesis: verum