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}) ;
then A1: IT c= union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } by Lm10;
now :: thesis: for x being object st x in IT holds
x in S -sequents
let x be object ; :: thesis: ( x in IT implies x in S -sequents )
reconsider xx = x as set by TARSKI:1;
assume x in IT ; :: thesis: x in S -sequents
then consider Y being set such that
A2: ( x in Y & Y in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ) by A1, TARSKI:def 4;
consider mm being Element of NAT such that
A3: Y = ((mm,D) -derivables) . X by A2;
xx is mm,X,D -derivable by A2, A3;
hence x in S -sequents by Def2; :: thesis: verum
end;
then IT c= S -sequents by TARSKI:def 3;
hence IT is S -sequents-like ; :: thesis: verum