set A = {(R#0 S),(R#1 S),(R#2 S),(R#3a S),(R#3b S),(R#3d S),(R#3e S),(R#4 S)};
set B = {(R#5 S),(R#6 S),(R#7 S),(R#8 S)};
set IT = S -rules ;
{(R#0 S),(R#1 S),(R#2 S),(R#3a S),(R#3b S),(R#3d S),(R#3e S),(R#4 S)} = {(R#0 S),(R#1 S),(R#2 S),(R#3a S)} \/ {(R#3b S),(R#3d S),(R#3e S),(R#4 S)} by ENUMSET1:25;
then reconsider AA = {(R#0 S),(R#1 S),(R#2 S),(R#3a S),(R#3b S),(R#3d S),(R#3e S),(R#4 S)} as isotone RuleSet of S ;
AA \/ {(R#5 S),(R#6 S),(R#7 S),(R#8 S)} is isotone ;
hence for b₁ being RuleSet of S st b₁ = S -rules holds
b₁ is isotone ; :: thesis: verum