theorem :: ORDINAL3:69

for A, B being Ordinal holds (A *^ B) mod^ B = {}