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 ;

now :: thesis: for P being Rule of S st P in S -rules holds
P is Correct

let P be Rule of S; :: thesis: ( P in S -rules implies P is Correct )
assume P in S -rules ; :: thesis: P is Correct
then ( P 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)} or P in {(R#5 S),(R#6 S),(R#7 S),(R#8 S)} ) by XBOOLE_0:def 3;
hence P is Correct by ENUMSET1:def 6, ENUMSET1:def 2; :: thesis: verum

end;

hence for b₁ being RuleSet of S st b₁ = S -rules holds
b₁ is Correct by Th14; :: thesis: verum