card I <> 0 ;
hence not DualBasis I is empty by ThDB1, CARD_1:27; :: thesis: verum