card (DualBasis I) c= card I by ThDB1;
hence DualBasis I is finite ; :: thesis: verum