{{}} is Subset of (Fin X) by FINSUB_1:7, ZFMISC_1:31;
hence not for b1 being Subset of (Fin X) holds b1 is empty ; :: thesis: verum