deffunc H₁( Relation) -> set = rng X;
defpred S₁[ set ] means X in X;
reconsider A = X \/ {{}} as functional non empty finite-membered set ;
set IT = { H₁(x) where x is Element of A : S₁[x] } ;

A1: now :: thesis: for y being set st y in { H₁(x) where x is Element of A : S₁[x] } holds
y is finite

let y be set ; :: thesis: ( y in { H₁(x) where x is Element of A : S₁[x] } implies y is finite )
assume y in { H₁(x) where x is Element of A : S₁[x] } ; :: thesis: y is finite
then consider x being Element of A such that
A2: ( y = H₁(x) & S₁[x] ) ;
thus y is finite by A2; :: thesis: verum

end;

card { H₁(x) where x is Element of A : S₁[x] } c= card X from TREES_2:sch 2();
then reconsider ITT = { H₁(x) where x is Element of A : S₁[x] } as finite-membered countable set by A1, FINSET_1:def 6, WAYBEL12:1;
union ITT = SymbolsOf X ;
hence for b₁ being set st b₁ = SymbolsOf X holds
b₁ is countable ; :: thesis: verum