set A = {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)};
set B = {(R5 S),(R6 S),(R7 S),(R8 S)};
set IT = S -rules ;
{(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} = {(R0 S),(R1 S),(R2 S),(R3a S)} \/ {(R3b S),(R3d S),(R3e S),(R4 S)} by ENUMSET1:25;
then reconsider AA = {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} as isotone RuleSet of S ;
AA \/ {(R5 S),(R6 S),(R7 S),(R8 S)} is isotone ;
hence for b₁ being RuleSet of S st b₁ = S -rules holds
b₁ is isotone ; :: thesis: verum