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 C = {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)};
( R0 S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} & R1 S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} & R2 S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} & R3a S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} & R3b S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} & R3d S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} & R3e S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} & R4 S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} & R5 S in {(R5 S),(R6 S),(R7 S),(R8 S)} & R6 S in {(R5 S),(R6 S),(R7 S),(R8 S)} & R7 S in {(R5 S),(R6 S),(R7 S),(R8 S)} & R8 S in {(R5 S),(R6 S),(R7 S),(R8 S)} ) by ENUMSET1:def 2, ENUMSET1:def 6;
then ( R0 S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} & R1 S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} & R2 S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} & R3a S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} & R3b S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} & R3d S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} & R3e S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} & R4 S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} & R5 S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} & R6 S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} & R7 S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} & R8 S in {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} ) by XBOOLE_0:def 3;
hence for b₁ being RuleSet of S st b₁ = S -rules holds
b₁ is 2 -ranked by DefRank; :: thesis: verum