let A, B, C be Ordinal; :: thesis: ( A in B *^ C implies ( A div^ C in B & A mod^ C in C ) )
A1: A = ((A div^ C) *^ C) +^ (A mod^ C) by Th65;
assume A2: A in B *^ C ; :: thesis: ( A div^ C in B & A mod^ C in C )
then C <> {} by ORDINAL2:38;
then A3: ex D being Ordinal st
( A = ((A div^ C) *^ C) +^ D & D in C ) by Def6;
then A4: (A div^ C) *^ C c= A by Th24;
assume ( not A div^ C in B or not A mod^ C in C ) ; :: thesis: contradiction
then B *^ C c= (A div^ C) *^ C by A3, A1, Th21, ORDINAL1:16, ORDINAL2:41;
hence contradiction by A2, A4, ORDINAL1:5; :: thesis: verum