let X be set ; :: thesis: for S being Language
for D being RuleSet of S holds union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }
let S be Language; :: thesis: for D being RuleSet of S holds union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }
let D be RuleSet of S; :: thesis: union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }
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});

per cases ( not X in bool (S -sequents) or X in bool (S -sequents) ) ;

suppose A1: not X in bool (S -sequents) ; :: thesis: union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }

then {X} misses bool (S -sequents) by ZFMISC_1:50;
then {X} /\ (dom ((OneStep D) [*])) = {} by XBOOLE_0:def 7, XBOOLE_1:63;
then ((OneStep D) [*]) .: {X} = ((OneStep D) [*]) .: {} by RELAT_1:112
.= {} ;
then reconsider E = ((OneStep D) [*]) .: {X} as empty set ;

now :: thesis: for x being object st x in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } holds
x in {{}}

let x be object ; :: thesis: ( x in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } implies x in {{}} )
assume x in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ; :: thesis: x in {{}}
then consider mm being Element of NAT such that
A2: x = ((mm,D) -derivables) . X ;
not X in dom ((mm,D) -derivables) by A1;
then x = {} by FUNCT_1:def 2, A2;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

then union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } c= union {{}} by ZFMISC_1:77, TARSKI:def 3;
then union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } c= {} ;
then ( union E = {} & union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } = {} ) ;
hence union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ; :: thesis: verum

end;

suppose A3: X in bool (S -sequents) ; :: thesis: union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }

then reconsider Seqts = X as Element of bool (S -sequents) ;
for Y being set st Y in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } holds
Y c= union (((OneStep D) [*]) .: {X})

proof

let Y be set ; :: thesis: ( Y in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } implies Y c= union (((OneStep D) [*]) .: {X}) )
assume Y in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ; :: thesis: Y c= union (((OneStep D) [*]) .: {X})
then consider mm being Element of NAT such that
A4: Y = ((mm,D) -derivables) . X ;
thus Y c= union (((OneStep D) [*]) .: {X}) by A4, A3, Lm9; :: thesis: verum

end;

then A5: union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } c= union (((OneStep D) [*]) .: {X}) by ZFMISC_1:76;

now :: thesis: for y being object st y in union (((OneStep D) [*]) .: {X}) holds
y in union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }

let y be object ; :: thesis: ( y in union (((OneStep D) [*]) .: {X}) implies y in union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } )
reconsider yy = y as set by TARSKI:1;
assume y in union (((OneStep D) [*]) .: {X}) ; :: thesis: y in union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }
then {y} c= union (((OneStep D) [*]) .: {X}) by ZFMISC_1:31;
then consider mm being Element of NAT such that
A6: yy is mm,Seqts,D -derivable by Lm8, Def7;
set Y = ((mm,D) -derivables) . Seqts;
( y in ((mm,D) -derivables) . Seqts & ((mm,D) -derivables) . Seqts in { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ) by A6;
hence y in union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } by TARSKI:def 4; :: thesis: verum

end;

then union (((OneStep D) [*]) .: {X}) c= union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } ;
hence union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum } by A5, XBOOLE_0:def 10; :: thesis: verum

end;

end;