let A, B be Ordinal; :: thesis: (A *^ B) mod^ B = {}
A1: A *^ {} = {} by ORDINAL2:38;
A2: (A *^ B) -^ (A *^ B) = {} by Th54;
{} -^ (((A *^ B) div^ B) *^ B) = {} by Th56;
hence (A *^ B) mod^ B = {} by A1, A2, Th68; :: thesis: verum