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