theorem Th93: :: NUMBER19:93

for n, c being Nat st c = card ((seq (n,100)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) holds
( c >= 72 & ( not c = 72 or n mod 30 = 9 or n mod 30 = 10 ) )