let m be Nat; :: thesis: for X being set
for S being Language
for D being RuleSet of S holds ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
let X be set ; :: thesis: for S being Language
for D being RuleSet of S holds ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
let S be Language; :: thesis: for D being RuleSet of S holds ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
let D be RuleSet of S; :: thesis: ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
set F = { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ;
set LH = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ;
set Q = S -sequents ;
set O = OneStep D;
set RH = union (((OneStep D) [*]) .: {X});
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
((mm,D) -derivables) . X in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ;
then ((mm,D) -derivables) . X c= union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } by ZFMISC_1:74;
hence ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X}) by Lm10; :: thesis: verum