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