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 C = {(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#5 S),(R#6 S),(R#7 S),(R#8 S)};
( R#0 S in {(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#1 S in {(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#2 S in {(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#3a S in {(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#3b S in {(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#3d S in {(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#3e S in {(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#4 S in {(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#5 S in {(R#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#6 S in {(R#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#7 S in {(R#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#8 S in {(R#5 S),(R#6 S),(R#7 S),(R#8 S)} ) by ENUMSET1:def 6, ENUMSET1:def 2;
then ( R#0 S in {(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#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#1 S in {(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#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#2 S in {(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#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#3a S in {(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#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#3b S in {(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#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#3d S in {(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#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#3e S in {(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#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#4 S in {(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#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#5 S in {(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#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#6 S in {(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#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#7 S in {(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#5 S),(R#6 S),(R#7 S),(R#8 S)} & R#8 S in {(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#5 S),(R#6 S),(R#7 S),(R#8 S)} ) by XBOOLE_0:def 3;
hence for b₁ being RuleSet of S st b₁ = S -rules holds
b₁ is 2 -ranked by Def62; :: thesis: verum