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