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 B0: x in ((m,D) -derivables) . X by DefDerivable3;
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X}) by Lm18b;
then {x} c= union (((OneStep D) [*]) .: {X}) by B0, ZFMISC_1:31;
hence {x} is X,D -derivable by DefDerivable; :: thesis: verum