let X be set ; :: thesis: for S being Language
for D being RuleSet of S st X c= S -sequents holds
(OneStep D) . X = union (union { (R .: {X}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D } )
let S be Language; :: thesis: for D being RuleSet of S st X c= S -sequents holds
(OneStep D) . X = union (union { (R .: {X}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D } )
let D be RuleSet of S; :: thesis: ( X c= S -sequents implies (OneStep D) . X = union (union { (R .: {X}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D } ) )
set Q = S -sequents ;
set F = { (R .: {X}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D } ;
set O = OneStep D;
assume X c= S -sequents ; :: thesis: (OneStep D) . X = union (union { (R .: {X}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D } )
then reconsider Seqts = X as Element of bool (S -sequents) ;
reconsider DD = D as Subset-Family of [:(bool (S -sequents)),(bool (S -sequents)):] by FOMODEL0:66;
(OneStep D) . Seqts = union ((union DD) .: {Seqts}) by Def5
.= union (union { (R .: {X}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D } ) by RELSET_2:34 ;
hence (OneStep D) . X = union (union { (R .: {X}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D } ) ; :: thesis: verum