let A, B, C, D be Ordinal; :: thesis: ( A c= B & C c= D implies A *^ C c= B *^ D )
assume ( A c= B & C c= D ) ; :: thesis: A *^ C c= B *^ D
then ( A *^ C c= B *^ C & B *^ C c= B *^ D ) by ORDINAL2:58, ORDINAL2:59;
hence A *^ C c= B *^ D by XBOOLE_1:1; :: thesis: verum