{r1,r2,r3,r4} = {r1,r2} \/ {r3,r4} by ENUMSET1:5;
hence for b₁ being RuleSet of S st b₁ = {r1,r2,r3,r4} holds
b₁ is isotone ; :: thesis: verum