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 for P being Rule of S st P in S -rules holds
P is Correct let P be
Rule of
S;
( P in S -rules implies P is Correct )assume
P in S -rules
;
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;
verum end;
hence
for b1 being RuleSet of S st b1 = S -rules holds
b1 is Correct
by Th14; verum