:: deftheorem Def5 defines OneStep FOMODEL4:def 5 :
for S being Language
for D being RuleSet of S
for b₃ being Rule of S holds
( b₃ = OneStep D iff for Seqs being Element of bool (S -sequents) holds b₃ . Seqs = union ((union D) .: {Seqs}) );