let B, A, C be Ordinal; :: thesis: ( B *^ A c= C *^ A & A <> {} implies B c= C )
A1: ( ( B *^ A c= C *^ A & B *^ A <> C *^ A ) iff B *^ A c< C *^ A ) by XBOOLE_0:def 8;
assume B *^ A c= C *^ A ; :: thesis: ( not A <> {} or B c= C )
then ( B *^ A = C *^ A or B *^ A in C *^ A ) by A1, ORDINAL1:21;
then not ( A <> {} & not B = C & not B in C ) by Th36, Th37;
hence ( not A <> {} or B c= C ) by ORDINAL1:def 2; :: thesis: verum