let m be Nat; :: thesis: for X being set
for S being Language
for D being RuleSet of S
for x being object st x is m,X,D -derivable holds
{x} is X,D -derivable
let X be set ; :: thesis: for S being Language
for D being RuleSet of S
for x being object st x is m,X,D -derivable holds
{x} is X,D -derivable
let S be Language; :: thesis: for D being RuleSet of S
for x being object st x is m,X,D -derivable holds
{x} is X,D -derivable
let D be RuleSet of S; :: thesis: for x being object st x is m,X,D -derivable holds
{x} is X,D -derivable
let x be object ; :: 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 ;
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X}) by Lm11;
hence {x} is X,D -derivable by A1, ZFMISC_1:31; :: thesis: verum