let m be Nat; :: thesis: for X being set
for S being Language
for D being RuleSet of S st X c= S -sequents 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 st X c= S -sequents holds
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
let S be Language; :: thesis: for D being RuleSet of S st X c= S -sequents holds
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
let D be RuleSet of S; :: thesis: ( X c= S -sequents implies ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X}) )
set O = OneStep D;
set RH = union (((OneStep D) [*]) .: {X});
set Q = S -sequents ;
assume X c= S -sequents ; :: thesis: ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
then B0: X in dom (iter ((OneStep D),m)) by Lm4;
reconsider f = union {(iter ((OneStep D),m))} as Function by ZFMISC_1:25;
B1: (iter ((OneStep D),m)) . X = union {((iter ((OneStep D),m)) . X)} by ZFMISC_1:25
.= union (Im ((iter ((OneStep D),m)),X)) by B0, FUNCT_1:59
.= union (f .: {X}) by ZFMISC_1:25 ;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
iter ((OneStep D),mm) = iter ((OneStep D),m) ;
then iter ((OneStep D),m) in D -iterators ;
then {(iter ((OneStep D),m))} c= D -iterators by ZFMISC_1:31;
then union {(iter ((OneStep D),m))} c= union (D -iterators) by ZFMISC_1:77;
then f .: {X} c= (union (D -iterators)) .: {X} by RELAT_1:124;
then B2: ((m,D) -derivables) . X c= union ((union (D -iterators)) .: {X}) by B1, ZFMISC_1:77;
rng (OneStep D) c= dom (OneStep D) by Lm4;
hence ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X}) by B2, FOMODEL0:17; :: thesis: verum