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