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 ;

now

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 {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} or P in {(R5 S),(R6 S),(R7 S),(R8 S)} ) by XBOOLE_0:def 3;
hence P is Correct by ENUMSET1:def 2, ENUMSET1:def 6; :: thesis: verum

end;

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