ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st T = [A,q] by Th72;
hence for b₁ being set st b₁ = T `1 holds
b₁ is finite ; :: thesis: verum