let m be Nat; :: thesis: for x, X being set
for S being Language
for D being RuleSet of S st x is m,X,D -derivable holds
{x} is X,D -derivable
let x, X be set ; :: thesis: for S being Language
for D being RuleSet of S st x is m,X,D -derivable holds
{x} is X,D -derivable
let S be Language; :: thesis: for D being RuleSet of S st x is m,X,D -derivable holds
{x} is X,D -derivable
let D be RuleSet of S; :: thesis: ( x is m,X,D -derivable implies {x} is X,D -derivable )
set Q = S -sequents ;
set O = OneStep D;
set RH = union (((OneStep D) [*]) .: {X});
assume x is m,X,D -derivable ; :: thesis: {x} is X,D -derivable
then A1: x in ((m,D) -derivables) . X by Def7;
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X}) by Lm11;
then {x} c= union (((OneStep D) [*]) .: {X}) by A1, ZFMISC_1:31;
hence {x} is X,D -derivable by Def6; :: thesis: verum