UBD (L~ (Cage (C,0))) in UBD-Family C ;
hence not UBD-Family C is empty ; :: thesis: verum