theorem Th97: :: NUMBER19:97

for n being Nat st 0 <= n & n < (2 * 3) * 5 holds
14 <= card ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))