let X be set ; 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; 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; ( 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 ) )
; union (((OneStep D1) [*]) .: {X}) c= union (((OneStep D2) [*]) .: {X})
now 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 ;
( 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 }
;
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;
verum end;
hence
union (((OneStep D1) [*]) .: {X}) c= union (((OneStep D2) [*]) .: {X})
by A1, ZFMISC_1:76; verum