[:[:A,B:],C:] is finite ;
hence [:A,B,C:] is finite by ZFMISC_1:def 3; :: thesis: verum