:: deftheorem defines multiples NUMBER14:def 16 :
for i being Integer holds multiples i = { m where m is Multiple of i : verum } ;