deffunc H1( Relation) -> set = rng X;
defpred S1[ set ] means X in X;
reconsider A = X \/ {{}} as functional non empty finite-membered set ;
set IT = { H1(x) where x is Element of A : S1[x] } ;
A1:
now for y being set st y in { H1(x) where x is Element of A : S1[x] } holds
y is finite let y be
set ;
( y in { H1(x) where x is Element of A : S1[x] } implies y is finite )assume
y in { H1(x) where x is Element of A : S1[x] }
;
y is finite then consider x being
Element of
A such that A2:
(
y = H1(
x) &
S1[
x] )
;
thus
y is
finite
by A2;
verum end;
card { H1(x) where x is Element of A : S1[x] } c= card X
from TREES_2:sch 2();
then reconsider ITT = { H1(x) where x is Element of A : S1[x] } as finite-membered countable set by A1, FINSET_1:def 6, WAYBEL12:1;
union ITT = SymbolsOf X
;
hence
for b1 being set st b1 = SymbolsOf X holds
b1 is countable
; verum