consider K being Cardinal;
Card ({} --> K) = {} --> K by Th8;
hence Card {} = {} ; :: thesis: verum