for A, B, C being Ordinal st A in B *^ C holds
( A div^ C in B & A mod^ C in C )