let X be set ; :: thesis: for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
union (((OneStep D1) [*]) .: {X}) c= union (((OneStep D2) [*]) .: {X})
let S be Language; :: thesis: for D1, D2 being RuleSet of S st D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
union (((OneStep D1) [*]) .: {X}) c= union (((OneStep D2) [*]) .: {X})
let D1, D2 be RuleSet of S; :: thesis: ( D1 c= D2 & ( D2 is isotone or D1 is isotone ) implies union (((OneStep D1) [*]) .: {X}) c= union (((OneStep D2) [*]) .: {X}) )
set F1 = { (((mm,D1) -derivables) . X) where mm is Element of NAT : verum } ;
set F2 = { (((mm,D2) -derivables) . X) where mm is Element of NAT : verum } ;
set O1 = OneStep D1;
set O2 = OneStep D2;
set Q = S -sequents ;
set LH = union (((OneStep D1) [*]) .: {X});
set RH = union (((OneStep D2) [*]) .: {X});
A1: ( union (((OneStep D1) [*]) .: {X}) = union { (((mm,D1) -derivables) . X) where mm is Element of NAT : verum } & union (((OneStep D2) [*]) .: {X}) = union { (((mm,D2) -derivables) . X) where mm is Element of NAT : verum } ) by Lm10;
assume A2: ( D1 c= D2 & ( D2 is isotone or D1 is isotone ) ) ; :: thesis: union (((OneStep D1) [*]) .: {X}) c= union (((OneStep D2) [*]) .: {X})

now :: thesis: for x being set st x in { (((mm,D1) -derivables) . X) where mm is Element of NAT : verum } holds
x c= union { (((mm,D2) -derivables) . X) where mm is Element of NAT : verum }

let x be set ; :: thesis: ( x in { (((mm,D1) -derivables) . X) where mm is Element of NAT : verum } implies x c= union { (((mm,D2) -derivables) . X) where mm is Element of NAT : verum } )
assume x in { (((mm,D1) -derivables) . X) where mm is Element of NAT : verum } ; :: thesis: x c= union { (((mm,D2) -derivables) . X) where mm is Element of NAT : verum }
then consider mm being Element of NAT such that
A3: x = ((mm,D1) -derivables) . X ;
A4: x c= ((mm,D2) -derivables) . X by A2, Lm16, A3;
((mm,D2) -derivables) . X in { (((mm,D2) -derivables) . X) where mm is Element of NAT : verum } ;
then ((mm,D2) -derivables) . X c= union { (((mm,D2) -derivables) . X) where mm is Element of NAT : verum } by ZFMISC_1:74;
hence x c= union { (((mm,D2) -derivables) . X) where mm is Element of NAT : verum } by A4, XBOOLE_1:1; :: thesis: verum

end;

hence union (((OneStep D1) [*]) .: {X}) c= union (((OneStep D2) [*]) .: {X}) by A1, ZFMISC_1:76; :: thesis: verum